1signature boolTools = 2sig 3 4include Abbrev 5 6 7val bool_eq_imp_CONV : conv; 8val bool_neg_pair_CONV : conv; 9val bool_imp_extract_CONV : conv; 10val REFL_IMP_CONV : conv; 11val GEN_IMP : term -> thm -> thm; 12 13 14val bool_eq_imp_ss : simpLib.ssfrag; 15val bool_neg_pair_ss : simpLib.ssfrag; 16val bool_imp_extract_ss : simpLib.ssfrag; 17 18val GEN_ASSUM : term -> thm -> thm; 19 20val STRENGTHEN_CONV_WRAPPER : conv -> conv; 21val DEPTH_STRENGTHEN_CONV : conv -> conv; 22val UNCHANGED_STRENGTHEN_CONV : conv -> conv; 23val ORELSE_STRENGTHEN_CONV : conv list -> conv; 24val CONJ_ASSUMPTIONS_STRENGTHEN_CONV : conv -> term list -> conv; 25 26 27val IMP_STRENGTHEN_CONV_RULE : conv -> rule; 28val STRENGTHEN_CONV_TAC : conv -> tactic; 29val DEPTH_STRENGTHEN_CONV_TAC : conv -> tactic; 30val CONJ_ASSUMPTIONS_DEPTH_STRENGTHEN_CONV : conv -> conv; 31 32 33 34val COND_REWR_CONV : thm -> term -> thm 35val COND_REWRITE_CONV : thm list -> term -> thm 36val GUARDED_COND_REWRITE_CONV : (term -> bool) -> thm list -> term -> thm 37 38end 39 40