PGEN_TAC
PairRules.PGEN_TAC : tactic
Strips the outermost paired universal quantifier from the conclusion of a goal.
When applied to a goal A ?- !p. t, the tactic PGEN_TAC reduces it to
A ?- t[p'/p] where p' is a variant of the paired variable structure
p chosen to avoid clashing with any variables free in the goal's
assumption list. Normally p' is just p.
A ?- !p. t
============== PGEN_TAC
A ?- t[p'/p]
Failure
Fails unless the goal's conclusion is a paired universally quantification.
See also
Tactic.GEN_TAC,
PairRules.FILTER_PGEN_TAC,
PairRules.PGEN,
PairRules.PGENL,
PairRules.PSPEC,
PairRules.PSPECL,
PairRules.PSPEC_ALL,
PairRules.PSPEC_TAC,
PairRules.PSTRIP_TAC,
PairRules.P_PGEN_TAC