FILTER_PGEN_TAC : (term -> tactic)
STRUCTURE
LIBRARY
pair
SYNOPSIS
Strips off a paired universal quantifier, but fails for a given quantified pair.
DESCRIPTION
When applied to a term q and a goal A ?- !p. t, the tactic FILTER_PGEN_TAC fails if the quantified pair p is the same as p, but otherwise advances the goal in the same way as PGEN_TAC, i.e. returns the goal A ?- t[p'/p] where p' is a variant of p chosen to avoid clashing with any variables free in the goal’s assumption list. Normally p' is just p.
     A ?- !p. t
   ==============  FILTER_PGEN_TAC "q"
    A ?- t[p'/p]

FAILURE
Fails if the goal’s conclusion is not a paired universal quantifier or the quantified pair is equal to the given term.
SEEALSO
HOL  Kananaskis-14