1signature quantHeuristicsTools =
2sig
3  include Abbrev
4
5
6  val TOP_ONCE_REWRITE_CONV        : thm list -> conv;
7  val NEG_NEG_INTRO_CONV           : conv;
8  val NEG_NEG_ELIM_CONV            : conv;
9  val NOT_FORALL_LIST_CONV         : conv;
10  val NOT_EXISTS_LIST_CONV         : conv;
11  val STRIP_NUM_QUANT_CONV         : int -> conv -> conv;
12  val BOUNDED_NOT_EXISTS_LIST_CONV : int -> conv;
13  val BOUNDED_REPEATC              : int -> conv -> conv;
14
15  val EXISTS_NOT_LIST_CONV         : conv;
16  val FORALL_NOT_LIST_CONV         : conv;
17  val QUANT_SIMP_CONV              : conv;
18
19  val NOT_OR_CONV                  : conv;
20  val NOT_AND_CONV                 : conv;
21  val AND_NOT_CONV                 : conv;
22  val OR_NOT_CONV                  : conv;
23
24  val VARIANT_TAC                  : term list -> tactic
25  val VARIANT_CONV                 : term list -> conv
26
27  val min_var_occur_CONV           : term -> conv
28  val match_term_var               : term -> term -> term -> term
29  val list_variant                 : term list -> term list -> (term list * (term,term) Lib.subst);
30
31  val EQ_EXISTS_INTRO              : (term * thm) -> thm;
32  val EQ_FORALL_INTRO              : (term * thm) -> thm;
33  val AND_IMP_INTRO_CONV           : term -> thm
34  val AND_IMP_ELIM_CONV            : term -> thm
35  val LIST_AND_IMP_ELIM_CONV       : term -> thm
36  val IMP_EXISTS_INTRO             : term * thm -> thm
37  val IMP_FORALL_INTRO             : term * thm -> thm
38  val LEFT_IMP_AND_INTRO_RULE      : term -> thm -> thm
39  val RIGHT_IMP_AND_INTRO_RULE     : term -> thm -> thm
40  val LEFT_IMP_OR_INTRO_RULE       : term -> thm -> thm
41  val RIGHT_IMP_OR_INTRO_RULE      : term -> thm -> thm
42
43end
44