1 (* |
|
2 ID: $Id$ |
|
3 *) |
|
4 |
|
5 (** legacy ML bindings **) |
|
6 |
|
7 val all_conj_distrib = thm "all_conj_distrib"; |
|
8 val all_simps = thms "all_simps"; |
|
9 val atomize_not = thm "atomize_not"; |
|
10 val case_split = thm "case_split_thm"; |
|
11 val case_split_thm = thm "case_split_thm" |
|
12 val cases_simp = thm "cases_simp"; |
|
13 val choice_eq = thm "choice_eq" |
|
14 val cong = thm "cong" |
|
15 val conj_comms = thms "conj_comms"; |
|
16 val conj_cong = thm "conj_cong"; |
|
17 val de_Morgan_conj = thm "de_Morgan_conj"; |
|
18 val de_Morgan_disj = thm "de_Morgan_disj"; |
|
19 val disj_assoc = thm "disj_assoc"; |
|
20 val disj_comms = thms "disj_comms"; |
|
21 val disj_cong = thm "disj_cong"; |
|
22 val eq_ac = thms "eq_ac"; |
|
23 val eq_cong2 = thm "eq_cong2" |
|
24 val Eq_FalseI = thm "Eq_FalseI"; |
|
25 val Eq_TrueI = thm "Eq_TrueI"; |
|
26 val Ex1_def = thm "Ex1_def" |
|
27 val ex_disj_distrib = thm "ex_disj_distrib"; |
|
28 val ex_simps = thms "ex_simps"; |
|
29 val if_cancel = thm "if_cancel"; |
|
30 val if_eq_cancel = thm "if_eq_cancel"; |
|
31 val if_False = thm "if_False"; |
|
32 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
|
33 val iff = thm "iff" |
|
34 val if_splits = thms "if_splits"; |
|
35 val if_True = thm "if_True"; |
|
36 val if_weak_cong = thm "if_weak_cong" |
|
37 val imp_all = thm "imp_all"; |
|
38 val imp_cong = thm "imp_cong"; |
|
39 val imp_conjL = thm "imp_conjL"; |
|
40 val imp_conjR = thm "imp_conjR"; |
|
41 val imp_conv_disj = thm "imp_conv_disj"; |
|
42 val simp_implies_def = thm "simp_implies_def"; |
|
43 val simp_thms = thms "simp_thms"; |
|
44 val split_if = thm "split_if"; |
|
45 val the1_equality = thm "the1_equality" |
|
46 val theI = thm "theI" |
|
47 val theI' = thm "theI'" |
|
48 val True_implies_equals = thm "True_implies_equals"; |
|