1\DOC RESTR_EVAL_RULE 2 3\TYPE {RESTR_EVAL_RULE : term list -> thm -> thm} 4 5\SYNOPSIS 6Symbolically evaluate a theorem, except for specified constants. 7 8\KEYWORDS 9evaluation. 10 11\DESCRIBE 12This is a version of {RESTR_EVAL_CONV} that works on theorems. 13 14\FAILURE 15As for {RESTR_EVAL_CONV}. 16 17\USES 18Controlling symbolic evaluation when it loops or becomes exponential. 19 20\SEEALSO 21bossLib.EVAL, bossLib.EVAL_RULE, computeLib.RESTR_EVAL_CONV, 22computeLib.RESTR_EVAL_TAC. 23 24\ENDDOC 25