RESTR_EVAL_TAC : term list -> tactic
STRUCTURE
computeLib
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
EVAL
,
EVAL_RULE
,
EVAL_TAC
,
RESTR_EVAL_CONV
,
RESTR_EVAL_RULE
HOL
Kananaskis-14