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