|
12999
|
1 |
(* legacy ML bindings *)
|
|
11749
|
2 |
|
|
21009
|
3 |
val prop_cs = HOL.claset_prop;
|
|
20973
|
4 |
val HOL_cs = HOL.claset;
|
|
|
5 |
val HOL_basic_ss = HOL.simpset_basic;
|
|
|
6 |
val HOL_ss = HOL.simpset;
|
|
|
7 |
val HOL_css = (HOL.claset, HOL.simpset);
|
|
|
8 |
val hol_simplify = HOL.simplify;
|
|
|
9 |
|
|
|
10 |
val split_tac = Splitter.split_tac;
|
|
|
11 |
val split_inside_tac = Splitter.split_inside_tac;
|
|
|
12 |
val split_asm_tac = Splitter.split_asm_tac;
|
|
|
13 |
val op addsplits = Splitter.addsplits;
|
|
|
14 |
val op delsplits = Splitter.delsplits;
|
|
|
15 |
val Addsplits = Splitter.Addsplits;
|
|
|
16 |
val Delsplits = Splitter.Delsplits;
|
|
|
17 |
|
|
20944
|
18 |
open HOL;
|
|
20973
|
19 |
val claset = Classical.claset;
|
|
|
20 |
val simpset = Simplifier.simpset;
|
|
|
21 |
val simplify = Simplifier.simplify;
|
|
21009
|
22 |
open Hypsubst;
|
|
|
23 |
open BasicClassical;
|
|
20973
|
24 |
open Clasimp;
|
|
12999
|
25 |
|
|
20944
|
26 |
val ext = thm "ext"
|
|
|
27 |
val True_def = thm "True_def"
|
|
|
28 |
val All_def = thm "All_def"
|
|
|
29 |
val Ex_def = thm "Ex_def"
|
|
|
30 |
val False_def = thm "False_def"
|
|
|
31 |
val not_def = thm "not_def"
|
|
|
32 |
val and_def = thm "and_def"
|
|
|
33 |
val or_def = thm "or_def"
|
|
|
34 |
val Ex1_def = thm "Ex1_def"
|
|
|
35 |
val iff = thm "iff"
|
|
|
36 |
val True_or_False = thm "True_or_False"
|
|
|
37 |
val Let_def = thm "Let_def"
|
|
|
38 |
val if_def = thm "if_def"
|
|
|
39 |
val ssubst = thm "ssubst"
|
|
|
40 |
val box_equals = thm "box_equals"
|
|
|
41 |
val fun_cong = thm "fun_cong"
|
|
|
42 |
val cong = thm "cong"
|
|
|
43 |
val rev_iffD2 = thm "rev_iffD2"
|
|
|
44 |
val rev_iffD1 = thm "rev_iffD1"
|
|
|
45 |
val iffE = thm "iffE"
|
|
|
46 |
val eqTrueI = thm "eqTrueI"
|
|
|
47 |
val eqTrueE = thm "eqTrueE"
|
|
|
48 |
val all_dupE = thm "all_dupE"
|
|
|
49 |
val FalseE = thm "FalseE"
|
|
|
50 |
val False_neq_True = thm "False_neq_True"
|
|
|
51 |
val False_not_True = thm "False_not_True"
|
|
|
52 |
val True_not_False = thm "True_not_False"
|
|
|
53 |
val notI2 = thm "notI2"
|
|
|
54 |
val impE = thm "impE"
|
|
|
55 |
val not_sym = thm "not_sym"
|
|
|
56 |
val rev_contrapos = thm "rev_contrapos"
|
|
|
57 |
val conjE = thm "conjE"
|
|
|
58 |
val context_conjI = thm "context_conjI"
|
|
|
59 |
val disjI1 = thm "disjI1"
|
|
|
60 |
val disjI2 = thm "disjI2"
|
|
|
61 |
val rev_notE = thm "rev_notE"
|
|
|
62 |
val ex1I = thm "ex1I"
|
|
|
63 |
val ex1E = thm "ex1E"
|
|
|
64 |
val ex1_implies_ex = thm "ex1_implies_ex"
|
|
|
65 |
val the_equality = thm "the_equality"
|
|
|
66 |
val theI = thm "theI"
|
|
|
67 |
val theI' = thm "theI'"
|
|
|
68 |
val theI2 = thm "theI2"
|
|
|
69 |
val the1_equality = thm "the1_equality"
|
|
|
70 |
val excluded_middle = thm "excluded_middle"
|
|
|
71 |
val case_split_thm = thm "case_split_thm"
|
|
|
72 |
val exCI = thm "exCI"
|
|
|
73 |
val choice_eq = thm "choice_eq"
|
|
|
74 |
val eq_cong2 = thm "eq_cong2"
|
|
|
75 |
val if_cong = thm "if_cong"
|
|
|
76 |
val if_weak_cong = thm "if_weak_cong"
|
|
|
77 |
val let_weak_cong = thm "let_weak_cong"
|
|
|
78 |
val eq_cong2 = thm "eq_cong2"
|
|
|
79 |
val if_distrib = thm "if_distrib"
|
|
|
80 |
val expand_case = thm "expand_case"
|
|
|
81 |
val restrict_to_left = thm "restrict_to_left"
|
|
|
82 |
val all_conj_distrib = thm "all_conj_distrib";
|
|
|
83 |
val atomize_not = thm "atomize_not";
|
|
|
84 |
val split_if = thm "split_if";
|
|
|
85 |
val split_if_asm = thm "split_if_asm";
|
|
|
86 |
val rev_conj_cong = thm "rev_conj_cong";
|
|
|
87 |
val not_all = thm "not_all";
|
|
|
88 |
val not_ex = thm "not_ex";
|
|
|
89 |
val not_iff = thm "not_iff";
|
|
|
90 |
val not_imp = thm "not_imp";
|
|
|
91 |
val not_not = thm "not_not";
|
|
|
92 |
val eta_contract_eq = thm "eta_contract_eq";
|
|
|
93 |
val eq_ac = thms "eq_ac";
|
|
|
94 |
val eq_commute = thm "eq_commute";
|
|
|
95 |
val eq_sym_conv = thm "eq_commute";
|
|
|
96 |
val neq_commute = thm "neq_commute";
|
|
|
97 |
val conj_comms = thms "conj_comms";
|
|
|
98 |
val conj_commute = thm "conj_commute";
|
|
|
99 |
val conj_cong = thm "conj_cong";
|
|
|
100 |
val conj_disj_distribL = thm "conj_disj_distribL";
|
|
|
101 |
val conj_disj_distribR = thm "conj_disj_distribR";
|
|
|
102 |
val conj_left_commute = thm "conj_left_commute";
|
|
|
103 |
val disj_comms = thms "disj_comms";
|
|
|
104 |
val disj_commute = thm "disj_commute";
|
|
|
105 |
val disj_cong = thm "disj_cong";
|
|
|
106 |
val disj_conj_distribL = thm "disj_conj_distribL";
|
|
|
107 |
val disj_conj_distribR = thm "disj_conj_distribR";
|
|
|
108 |
val disj_left_commute = thm "disj_left_commute";
|
|
|
109 |
val eq_assoc = thm "eq_assoc";
|
|
|
110 |
val eq_left_commute = thm "eq_left_commute";
|
|
|
111 |
val ex_disj_distrib = thm "ex_disj_distrib";
|
|
|
112 |
val if_P = thm "if_P";
|
|
|
113 |
val if_bool_eq_disj = thm "if_bool_eq_disj";
|
|
|
114 |
val if_def2 = thm "if_bool_eq_conj";
|
|
|
115 |
val if_not_P = thm "if_not_P";
|
|
|
116 |
val if_splits = thms "if_splits";
|
|
|
117 |
val imp_all = thm "imp_all";
|
|
|
118 |
val imp_conjL = thm "imp_conjL";
|
|
|
119 |
val imp_conjR = thm "imp_conjR";
|
|
|
120 |
val imp_disj_not1 = thm "imp_disj_not1";
|
|
|
121 |
val imp_disj_not2 = thm "imp_disj_not2";
|
|
|
122 |
val imp_ex = thm "imp_ex";
|
|
|
123 |
val meta_eq_to_obj_eq = thm "def_imp_eq";
|
|
|
124 |
val ex_simps = thms "ex_simps";
|
|
|
125 |
val all_simps = thms "all_simps";
|
|
|
126 |
val simp_thms = thms "simp_thms";
|
|
|
127 |
val Eq_FalseI = thm "Eq_FalseI";
|
|
|
128 |
val Eq_TrueI = thm "Eq_TrueI";
|
|
|
129 |
val cases_simp = thm "cases_simp";
|
|
|
130 |
val conj_assoc = thm "conj_assoc";
|
|
|
131 |
val de_Morgan_conj = thm "de_Morgan_conj";
|
|
|
132 |
val de_Morgan_disj = thm "de_Morgan_disj";
|
|
|
133 |
val disj_assoc = thm "disj_assoc";
|
|
|
134 |
val disj_not1 = thm "disj_not1";
|
|
|
135 |
val disj_not2 = thm "disj_not2";
|
|
|
136 |
val if_False = thm "if_False";
|
|
|
137 |
val if_True = thm "if_True";
|
|
|
138 |
val if_bool_eq_conj = thm "if_bool_eq_conj";
|
|
|
139 |
val if_cancel = thm "if_cancel";
|
|
|
140 |
val if_eq_cancel = thm "if_eq_cancel";
|
|
|
141 |
val iff_conv_conj_imp = thm "iff_conv_conj_imp";
|
|
|
142 |
val imp_cong = thm "imp_cong";
|
|
|
143 |
val imp_conv_disj = thm "imp_conv_disj";
|
|
|
144 |
val imp_disj1 = thm "imp_disj1";
|
|
|
145 |
val imp_disj2 = thm "imp_disj2";
|
|
|
146 |
val imp_disjL = thm "imp_disjL";
|
|
|
147 |
val simp_impliesI = thm "simp_impliesI";
|
|
|
148 |
val simp_implies_cong = thm "simp_implies_cong";
|
|
|
149 |
val simp_implies_def = thm "simp_implies_def";
|
|
|
150 |
val True_implies_equals = thm "True_implies_equals";
|
|
18916
|
151 |
|
|
|
152 |
structure HOL =
|
|
|
153 |
struct
|
|
|
154 |
|
|
|
155 |
open HOL;
|
|
|
156 |
|
|
|
157 |
val thy = the_context ();
|
|
|
158 |
|
|
|
159 |
end;
|