1signature pairTools = 2sig 3 include Abbrev 4 5 val PairCases : tactic 6 val PairCases_on : term quotation -> tactic 7 val PGEN : term -> term -> thm -> thm 8 val PGEN_TAC : term -> tactic 9 val PFUN_EQ_RULE : thm -> thm 10 11 val PAIR_EX : term -> term -> thm 12 13 val LET_INTRO : thm -> thm 14 val LET_INTRO_TAC : tactic 15 val LET_EQ_TAC : thm list -> tactic 16 val TUPLE : term -> thm -> thm 17 val TUPLE_TAC : term -> tactic 18 val SPLIT_QUANT_CONV : term -> conv 19 val ELIM_TUPLED_QUANT_CONV : conv 20 val INTRO_TUPLED_QUANT_CONV : conv 21 22 val PABS_ELIM_CONV : conv 23 val PABS_INTRO_CONV : term -> conv 24 25end 26