RESTR_EVAL_RULE
computeLib.RESTR_EVAL_RULE : term list -> thm -> thm
Symbolically evaluate a theorem, except for specified constants.
This is a version of RESTR_EVAL_CONV that works on theorems.
Failure
As for RESTR_EVAL_CONV.
Controlling symbolic evaluation when it loops or becomes exponential.
See also
bossLib.EVAL,
bossLib.EVAL_RULE,
computeLib.RESTR_EVAL_CONV,
computeLib.RESTR_EVAL_TAC