1\DOC RESTR_EVAL_TAC 2 3\TYPE {RESTR_EVAL_TAC : term list -> tactic} 4 5\SYNOPSIS 6Symbolically evaluate a theorem, except for specified constants. 7 8\KEYWORDS 9evaluation. 10 11\DESCRIBE 12This is a tactic version of {RESTR_EVAL_CONV}. 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, bossLib.EVAL_TAC, 22computeLib.RESTR_EVAL_CONV, computeLib.RESTR_EVAL_RULE. 23 24\ENDDOC 25