PGEN_TAC : tactic
STRUCTURE
LIBRARY
pair
SYNOPSIS
Strips the outermost paired universal quantifier from the conclusion of a goal.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1