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