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