RESTR_EVAL_TAC : term list -> tactic
STRUCTURE
SYNOPSIS
Symbolically evaluate a theorem, except for specified constants.
DESCRIPTION
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
HOL  Trindemossen-1