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