author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Wed, 07 Sep 2011 07:59:45 +0900 | |
changeset 44763 | b50d5d694838 |
parent 39302 | d7728f65b353 |
permissions | -rw-r--r-- |
14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"RES_SELECT" > "RES_SELECT_def" |
|
7 |
"RES_FORALL" > "RES_FORALL_def" |
|
8 |
"RES_EXISTS_UNIQUE" > "RES_EXISTS_UNIQUE_def" |
|
9 |
"RES_EXISTS" > "RES_EXISTS_def" |
|
10 |
"RES_ABSTRACT" > "RES_ABSTRACT_def" |
|
11 |
"IN" > "IN_def" |
|
12 |
"ARB" > "ARB_def" |
|
13 |
||
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
14 |
type_maps |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
15 |
"bool" > "HOL.bool" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
16 |
|
14516 | 17 |
const_maps |
38556 | 18 |
"~" > "HOL.Not" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
19 |
"bool_case" > "Product_Type.bool.bool_case" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
20 |
"\\/" > "HOL.disj" |
14516 | 21 |
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" |
38556 | 22 |
"T" > "HOL.True" |
14516 | 23 |
"RES_SELECT" > "HOL4Base.bool.RES_SELECT" |
24 |
"RES_FORALL" > "HOL4Base.bool.RES_FORALL" |
|
25 |
"RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE" |
|
26 |
"RES_EXISTS" > "HOL4Base.bool.RES_EXISTS" |
|
17644 | 27 |
"ONTO" > "Fun.surj" |
14516 | 28 |
"ONE_ONE" > "HOL4Setup.ONE_ONE" |
29 |
"LET" > "HOL4Compat.LET" |
|
30 |
"IN" > "HOL4Base.bool.IN" |
|
38556 | 31 |
"F" > "HOL.False" |
16587 | 32 |
"COND" > "HOL.If" |
14516 | 33 |
"ARB" > "HOL4Base.bool.ARB" |
38556 | 34 |
"?!" > "HOL.Ex1" |
35 |
"?" > "HOL.Ex" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
36 |
"/\\" > "HOL.conj" |
38556 | 37 |
"!" > "HOL.All" |
14516 | 38 |
|
39 |
thm_maps |
|
40 |
"bool_case_thm" > "HOL4Base.bool.bool_case_thm" |
|
41 |
"bool_case_ID" > "HOL4Base.bool.bool_case_ID" |
|
42 |
"bool_case_DEF" > "HOL4Compat.bool_case_DEF" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
43 |
"bool_INDUCT" > "Product_Type.bool.induct" |
14516 | 44 |
"boolAxiom" > "HOL4Base.bool.boolAxiom" |
45 |
"UNWIND_THM2" > "HOL.simp_thms_39" |
|
46 |
"UNWIND_THM1" > "HOL.simp_thms_40" |
|
17652 | 47 |
"UNWIND_FORALL_THM2" > "HOL.simp_thms_41" |
14516 | 48 |
"UNWIND_FORALL_THM1" > "HOL.simp_thms_42" |
49 |
"UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP" |
|
50 |
"UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM" |
|
51 |
"T_DEF" > "HOL.True_def" |
|
52 |
"TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION" |
|
53 |
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" |
|
54 |
"TRUTH" > "HOL.TrueI" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
55 |
"SWAP_FORALL_THM" > "HOL.all_comm" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
56 |
"SWAP_EXISTS_THM" > "HOL.ex_comm" |
14516 | 57 |
"SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM" |
58 |
"SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE" |
|
59 |
"SELECT_THM" > "HOL4Setup.EXISTS_DEF" |
|
60 |
"SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial" |
|
61 |
"SELECT_REFL" > "Hilbert_Choice.some_eq_trivial" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
62 |
"SELECT_AX" > "Hilbert_Choice.someI" |
14516 | 63 |
"RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR" |
64 |
"RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4" |
|
65 |
"RIGHT_FORALL_OR_THM" > "HOL.all_simps_4" |
|
66 |
"RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6" |
|
67 |
"RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6" |
|
68 |
"RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
69 |
"RIGHT_AND_OVER_OR" > "Groebner_Basis.dnf_2" |
14516 | 70 |
"RIGHT_AND_FORALL_THM" > "HOL.all_simps_2" |
71 |
"RES_SELECT_def" > "HOL4Base.bool.RES_SELECT_def" |
|
72 |
"RES_SELECT_DEF" > "HOL4Base.bool.RES_SELECT_DEF" |
|
73 |
"RES_FORALL_def" > "HOL4Base.bool.RES_FORALL_def" |
|
74 |
"RES_FORALL_DEF" > "HOL4Base.bool.RES_FORALL_DEF" |
|
75 |
"RES_EXISTS_def" > "HOL4Base.bool.RES_EXISTS_def" |
|
76 |
"RES_EXISTS_UNIQUE_def" > "HOL4Base.bool.RES_EXISTS_UNIQUE_def" |
|
77 |
"RES_EXISTS_UNIQUE_DEF" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF" |
|
78 |
"RES_EXISTS_DEF" > "HOL4Base.bool.RES_EXISTS_DEF" |
|
79 |
"RES_ABSTRACT_DEF" > "HOL4Base.bool.RES_ABSTRACT_DEF" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
80 |
"REFL_CLAUSE" > "Groebner_Basis.bool_simps_6" |
14516 | 81 |
"OR_INTRO_THM2" > "HOL.disjI2" |
82 |
"OR_INTRO_THM1" > "HOL.disjI1" |
|
83 |
"OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
84 |
"OR_ELIM_THM" > "HOL.disjE" |
14516 | 85 |
"OR_DEF" > "HOL.or_def" |
86 |
"OR_CONG" > "HOL4Base.bool.OR_CONG" |
|
87 |
"OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES" |
|
17644 | 88 |
"ONTO_THM" > "Fun.surj_def" |
89 |
"ONTO_DEF" > "Fun.surj_def" |
|
14516 | 90 |
"ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM" |
91 |
"ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF" |
|
92 |
"NOT_IMP" > "HOL.not_imp" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
93 |
"NOT_FORALL_THM" > "HOL.not_all" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
94 |
"NOT_F" > "Groebner_Basis.PFalse_2" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
95 |
"NOT_EXISTS_THM" > "HOL.not_ex" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
96 |
"NOT_DEF" > "Groebner_Basis.bool_simps_19" |
14516 | 97 |
"NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES" |
98 |
"NOT_AND" > "HOL4Base.bool.NOT_AND" |
|
17188 | 99 |
"MONO_OR" > "Inductive.basic_monos_3" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
100 |
"MONO_NOT" > "HOL.contrapos_nn" |
17652 | 101 |
"MONO_IMP" > "Set.imp_mono" |
17188 | 102 |
"MONO_EXISTS" > "Inductive.basic_monos_5" |
14516 | 103 |
"MONO_COND" > "HOL4Base.bool.MONO_COND" |
17188 | 104 |
"MONO_AND" > "Inductive.basic_monos_4" |
14516 | 105 |
"MONO_ALL" > "Inductive.basic_monos_6" |
106 |
"LET_THM" > "HOL.Let_def" |
|
107 |
"LET_RATOR" > "HOL4Base.bool.LET_RATOR" |
|
108 |
"LET_RAND" > "HOL4Base.bool.LET_RAND" |
|
109 |
"LET_DEF" > "HOL4Compat.LET_def" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
110 |
"LET_CONG" > "FunDef.let_cong" |
14516 | 111 |
"LEFT_OR_OVER_AND" > "HOL.disj_conj_distribL" |
112 |
"LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3" |
|
113 |
"LEFT_FORALL_OR_THM" > "HOL.all_simps_3" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
114 |
"LEFT_FORALL_IMP_THM" > "HOL.all_simps_5" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
115 |
"LEFT_EXISTS_IMP_THM" > "HOL.ex_simps_5" |
14516 | 116 |
"LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
117 |
"LEFT_AND_OVER_OR" > "Groebner_Basis.dnf_1" |
17652 | 118 |
"LEFT_AND_FORALL_THM" > "HOL.all_simps_1" |
14516 | 119 |
"IN_def" > "HOL4Base.bool.IN_def" |
120 |
"IN_DEF" > "HOL4Base.bool.IN_DEF" |
|
121 |
"INFINITY_AX" > "HOL4Setup.INFINITY_AX" |
|
122 |
"IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F" |
|
123 |
"IMP_F" > "HOL.notI" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
124 |
"IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3" |
14516 | 125 |
"IMP_CONG" > "HOL.imp_cong" |
126 |
"IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
127 |
"IMP_ANTISYM_AX" > "HOL.iff" |
14516 | 128 |
"F_IMP" > "HOL4Base.bool.F_IMP" |
129 |
"F_DEF" > "HOL.False_def" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
130 |
"FUN_EQ_THM" > "HOL.fun_eq_iff" |
14516 | 131 |
"FORALL_THM" > "HOL4Base.bool.FORALL_THM" |
132 |
"FORALL_SIMP" > "HOL.simp_thms_35" |
|
133 |
"FORALL_DEF" > "HOL.All_def" |
|
134 |
"FORALL_AND_THM" > "HOL.all_conj_distrib" |
|
135 |
"FALSITY" > "HOL.FalseE" |
|
136 |
"EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF" |
|
137 |
"EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1" |
|
138 |
"EXISTS_UNIQUE_DEF" > "HOL4Compat.EXISTS_UNIQUE_DEF" |
|
139 |
"EXISTS_THM" > "HOL4Base.bool.EXISTS_THM" |
|
140 |
"EXISTS_SIMP" > "HOL.simp_thms_36" |
|
141 |
"EXISTS_REFL" > "HOL.simp_thms_37" |
|
142 |
"EXISTS_OR_THM" > "HOL.ex_disj_distrib" |
|
143 |
"EXISTS_DEF" > "HOL4Setup.EXISTS_DEF" |
|
144 |
"EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
145 |
"ETA_THM" > "HOL.eta_contract_eq" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
146 |
"ETA_AX" > "HOL.eta_contract_eq" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
147 |
"EQ_TRANS" > "HOL.trans" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
148 |
"EQ_SYM_EQ" > "HOL.eq_ac_1" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
149 |
"EQ_SYM" > "HOL.eq_reflection" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
150 |
"EQ_REFL" > "HOL.refl" |
14516 | 151 |
"EQ_IMP_THM" > "HOL.iff_conv_conj_imp" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
152 |
"EQ_EXT" > "HOL.eq_reflection" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
153 |
"EQ_EXPAND" > "Groebner_Basis.nnf_simps_4" |
14516 | 154 |
"EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
155 |
"DISJ_SYM" > "Groebner_Basis.dnf_4" |
14516 | 156 |
"DISJ_IMP_THM" > "HOL.imp_disjL" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
157 |
"DISJ_COMM" > "Groebner_Basis.dnf_4" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
158 |
"DISJ_ASSOC" > "HOL.disj_ac_3" |
14516 | 159 |
"DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
160 |
"CONJ_SYM" > "Groebner_Basis.dnf_3" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
161 |
"CONJ_COMM" > "Groebner_Basis.dnf_3" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
162 |
"CONJ_ASSOC" > "HOL.conj_ac_3" |
14516 | 163 |
"COND_RATOR" > "HOL4Base.bool.COND_RATOR" |
164 |
"COND_RAND" > "HOL.if_distrib" |
|
165 |
"COND_ID" > "HOL.if_cancel" |
|
166 |
"COND_EXPAND" > "HOL4Base.bool.COND_EXPAND" |
|
167 |
"COND_DEF" > "HOL4Compat.COND_DEF" |
|
168 |
"COND_CONG" > "HOL4Base.bool.COND_CONG" |
|
169 |
"COND_CLAUSES" > "HOL4Base.bool.COND_CLAUSES" |
|
170 |
"COND_ABS" > "HOL4Base.bool.COND_ABS" |
|
171 |
"BOTH_FORALL_OR_THM" > "HOL4Base.bool.BOTH_FORALL_OR_THM" |
|
172 |
"BOTH_FORALL_IMP_THM" > "HOL4Base.bool.BOTH_FORALL_IMP_THM" |
|
173 |
"BOTH_EXISTS_IMP_THM" > "HOL4Base.bool.BOTH_EXISTS_IMP_THM" |
|
174 |
"BOTH_EXISTS_AND_THM" > "HOL4Base.bool.BOTH_EXISTS_AND_THM" |
|
175 |
"BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT" |
|
176 |
"BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM" |
|
177 |
"BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
178 |
"BOOL_CASES_AX" > "HOL.True_or_False" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
179 |
"BETA_THM" > "HOL.eta_contract_eq" |
14516 | 180 |
"ARB_def" > "HOL4Base.bool.ARB_def" |
181 |
"ARB_DEF" > "HOL4Base.bool.ARB_DEF" |
|
182 |
"AND_INTRO_THM" > "HOL.conjI" |
|
183 |
"AND_IMP_INTRO" > "HOL.imp_conjL" |
|
184 |
"AND_DEF" > "HOL.and_def" |
|
185 |
"AND_CONG" > "HOL4Base.bool.AND_CONG" |
|
186 |
"AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES" |
|
187 |
"AND2_THM" > "HOL.conjunct2" |
|
188 |
"AND1_THM" > "HOL.conjunct1" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
189 |
"ABS_SIMP" > "HOL.refl" |
14516 | 190 |
"ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM" |
191 |
||
192 |
ignore_thms |
|
193 |
"UNBOUNDED_THM" |
|
194 |
"UNBOUNDED_DEF" |
|
195 |
"BOUNDED_THM" |
|
196 |
"BOUNDED_DEF" |
|
197 |
||
198 |
end |