----------------------------------------------------------------------
RESTR_EVAL_RULE                                           (computeLib)
----------------------------------------------------------------------
RESTR_EVAL_RULE : term list -> thm -> thm

SYNOPSIS
Symbolically evaluate a theorem, except for specified constants.

KEYWORDS
evaluation.

DESCRIBE
This is a version of {RESTR_EVAL_CONV} that works on theorems.

FAILURE
As for {RESTR_EVAL_CONV}.

USES
Controlling symbolic evaluation when it loops or becomes exponential.

SEEALSO
bossLib.EVAL, bossLib.EVAL_RULE, computeLib.RESTR_EVAL_CONV,
computeLib.RESTR_EVAL_TAC.

----------------------------------------------------------------------