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