RECALL_ACCEPT_TAC : ('a -> thm) -> 'a -> goal -> goalstate
Delay evaluation of theorem-producing function till needed.
Given a theorem-producing inference rule f and its argument a, the tactic
RECALL_ACCEPT_TAC f a will evaluate th = f a and do ACCEPT_TAC th, but
only when the tactic is applied to a goal.
- FAILURE CONDITIONS
Never fails until subsequently applied to a goal, but then may fail if the
theorem-producing function does.
You might for example do
and the call
RECALL_ACCEPT_TAC (EQT_ELIM o NUM_REDUCE_CONV) `16 EXP 53 < 15 EXP 55`;;
will be delayed until the tactic is applied.
(EQT_ELIM o NUM_REDUCE_CONV) `16 EXP 53 < 15 EXP 55`
Delaying a time-consuming compound inference rule in a tactic script until it
is actually used.