RESTR_EVAL_RULE : term list -> thm -> thm
STRUCTURE
SYNOPSIS
Symbolically evaluate a theorem, except for specified constants.
DESCRIPTION
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
HOL  Kananaskis-13