\DOC RESTR_EVAL_TAC

\TYPE {RESTR_EVAL_TAC : term list -> tactic}

\SYNOPSIS
Symbolically evaluate a theorem, except for specified constants.

\KEYWORDS
evaluation.

\DESCRIBE
This is a tactic version of {RESTR_EVAL_CONV}.

\FAILURE
As for {RESTR_EVAL_CONV}.

\USES
Controlling symbolic evaluation when it loops or becomes exponential.

\SEEALSO
bossLib.EVAL, bossLib.EVAL_RULE, bossLib.EVAL_TAC,
computeLib.RESTR_EVAL_CONV, computeLib.RESTR_EVAL_RULE.

\ENDDOC