META_SPEC_TAC : term -> thm -> tactic
Replaces universally quantified variable in theorem with metavariable.
Given a variable v and a theorem th of the form A |- !x. p[x], the
tactic META_SPEC_TAC `v` th is a tactic that adds the theorem A |- p[v] to
the assumptions of the goal, with v a new metavariable. This can later be
instantiated, e.g. by UNIFY_ACCEPT_TAC, and it is as if the instantiation
were done at this point.
- FAILURE CONDITIONS
Fails if v is not a variable.
See UNIFY_ACCEPT_TAC for an example of using metavariables.
Delaying instantiations until the right choice becomes clearer.
Users should probably steer clear of using metavariables if possible. Note that
the metavariable instantiations apply across the whole fringe of goals, not
just the current goal, and can lead to confusion.
- SEE ALSO
EXISTS_TAC, EXISTS_TAC, UNIFY_ACCEPT_TAC, X_META_EXISTS_TAC.