PCHOOSE_TAC : thm_tactic
STRUCTURE
LIBRARY
pair
SYNOPSIS
Adds the body of a paired existentially quantified theorem to the assumptions of a goal.
DESCRIPTION
When applied to a theorem A' |- ?p. t and a goal, CHOOSE_TAC adds t[p'/p] to the assumptions of the goal, where p' is a variant of the pair p which has no components free in the assumption list; normally p' is just p.
         A ?- u
   ====================  CHOOSE_TAC (A' |- ?q. t)
    A u {t[p'/p]} ?- u
Unless A' is a subset of A, this is not a valid tactic.
FAILURE
Fails unless the given theorem is a paired existential quantification.
SEEALSO
HOL  Trindemossen-1