author | nipkow |
Mon, 13 Sep 2010 11:13:15 +0200 | |
changeset 39302 | d7728f65b353 |
parent 39198 | f967a16dfcdd |
child 44763 | b50d5d694838 |
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 |
||
14 |
const_maps |
|
38556 | 15 |
"~" > "HOL.Not" |
14516 | 16 |
"bool_case" > "Datatype.bool.bool_case" |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38556
diff
changeset
|
17 |
"\\/" > HOL.disj |
14516 | 18 |
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" |
38556 | 19 |
"T" > "HOL.True" |
14516 | 20 |
"RES_SELECT" > "HOL4Base.bool.RES_SELECT" |
21 |
"RES_FORALL" > "HOL4Base.bool.RES_FORALL" |
|
22 |
"RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE" |
|
23 |
"RES_EXISTS" > "HOL4Base.bool.RES_EXISTS" |
|
17644 | 24 |
"ONTO" > "Fun.surj" |
14516 | 25 |
"ONE_ONE" > "HOL4Setup.ONE_ONE" |
26 |
"LET" > "HOL4Compat.LET" |
|
27 |
"IN" > "HOL4Base.bool.IN" |
|
38556 | 28 |
"F" > "HOL.False" |
16587 | 29 |
"COND" > "HOL.If" |
14516 | 30 |
"ARB" > "HOL4Base.bool.ARB" |
38556 | 31 |
"?!" > "HOL.Ex1" |
32 |
"?" > "HOL.Ex" |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38556
diff
changeset
|
33 |
"/\\" > HOL.conj |
38556 | 34 |
"!" > "HOL.All" |
14516 | 35 |
|
36 |
thm_maps |
|
37 |
"bool_case_thm" > "HOL4Base.bool.bool_case_thm" |
|
38 |
"bool_case_ID" > "HOL4Base.bool.bool_case_ID" |
|
39 |
"bool_case_DEF" > "HOL4Compat.bool_case_DEF" |
|
17916 | 40 |
"bool_INDUCT" > "Datatype.bool.induct_correctness" |
14516 | 41 |
"boolAxiom" > "HOL4Base.bool.boolAxiom" |
42 |
"UNWIND_THM2" > "HOL.simp_thms_39" |
|
43 |
"UNWIND_THM1" > "HOL.simp_thms_40" |
|
17652 | 44 |
"UNWIND_FORALL_THM2" > "HOL.simp_thms_41" |
14516 | 45 |
"UNWIND_FORALL_THM1" > "HOL.simp_thms_42" |
46 |
"UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP" |
|
47 |
"UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM" |
|
48 |
"T_DEF" > "HOL.True_def" |
|
49 |
"TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION" |
|
50 |
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" |
|
51 |
"TRUTH" > "HOL.TrueI" |
|
52 |
"SWAP_FORALL_THM" > "HOL4Base.bool.SWAP_FORALL_THM" |
|
53 |
"SWAP_EXISTS_THM" > "HOL4Base.bool.SWAP_EXISTS_THM" |
|
54 |
"SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM" |
|
55 |
"SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE" |
|
56 |
"SELECT_THM" > "HOL4Setup.EXISTS_DEF" |
|
57 |
"SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial" |
|
58 |
"SELECT_REFL" > "Hilbert_Choice.some_eq_trivial" |
|
59 |
"SELECT_AX" > "Hilbert_Choice.tfl_some" |
|
60 |
"RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR" |
|
61 |
"RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4" |
|
62 |
"RIGHT_FORALL_OR_THM" > "HOL.all_simps_4" |
|
63 |
"RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6" |
|
64 |
"RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6" |
|
65 |
"RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2" |
|
66 |
"RIGHT_AND_OVER_OR" > "HOL.conj_disj_distribR" |
|
67 |
"RIGHT_AND_FORALL_THM" > "HOL.all_simps_2" |
|
68 |
"RES_SELECT_def" > "HOL4Base.bool.RES_SELECT_def" |
|
69 |
"RES_SELECT_DEF" > "HOL4Base.bool.RES_SELECT_DEF" |
|
70 |
"RES_FORALL_def" > "HOL4Base.bool.RES_FORALL_def" |
|
71 |
"RES_FORALL_DEF" > "HOL4Base.bool.RES_FORALL_DEF" |
|
72 |
"RES_EXISTS_def" > "HOL4Base.bool.RES_EXISTS_def" |
|
73 |
"RES_EXISTS_UNIQUE_def" > "HOL4Base.bool.RES_EXISTS_UNIQUE_def" |
|
74 |
"RES_EXISTS_UNIQUE_DEF" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF" |
|
75 |
"RES_EXISTS_DEF" > "HOL4Base.bool.RES_EXISTS_DEF" |
|
76 |
"RES_ABSTRACT_DEF" > "HOL4Base.bool.RES_ABSTRACT_DEF" |
|
77 |
"REFL_CLAUSE" > "HOL.simp_thms_6" |
|
78 |
"OR_INTRO_THM2" > "HOL.disjI2" |
|
79 |
"OR_INTRO_THM1" > "HOL.disjI1" |
|
80 |
"OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM" |
|
17188 | 81 |
"OR_ELIM_THM" > "Recdef.tfl_disjE" |
14516 | 82 |
"OR_DEF" > "HOL.or_def" |
83 |
"OR_CONG" > "HOL4Base.bool.OR_CONG" |
|
84 |
"OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES" |
|
17644 | 85 |
"ONTO_THM" > "Fun.surj_def" |
86 |
"ONTO_DEF" > "Fun.surj_def" |
|
14516 | 87 |
"ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM" |
88 |
"ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF" |
|
89 |
"NOT_IMP" > "HOL.not_imp" |
|
90 |
"NOT_FORALL_THM" > "Inductive.basic_monos_15" |
|
91 |
"NOT_F" > "HOL.Eq_FalseI" |
|
92 |
"NOT_EXISTS_THM" > "Inductive.basic_monos_16" |
|
93 |
"NOT_DEF" > "HOL.simp_thms_19" |
|
94 |
"NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES" |
|
95 |
"NOT_AND" > "HOL4Base.bool.NOT_AND" |
|
17188 | 96 |
"MONO_OR" > "Inductive.basic_monos_3" |
14516 | 97 |
"MONO_NOT" > "HOL.rev_contrapos" |
17652 | 98 |
"MONO_IMP" > "Set.imp_mono" |
17188 | 99 |
"MONO_EXISTS" > "Inductive.basic_monos_5" |
14516 | 100 |
"MONO_COND" > "HOL4Base.bool.MONO_COND" |
17188 | 101 |
"MONO_AND" > "Inductive.basic_monos_4" |
14516 | 102 |
"MONO_ALL" > "Inductive.basic_monos_6" |
103 |
"LET_THM" > "HOL.Let_def" |
|
104 |
"LET_RATOR" > "HOL4Base.bool.LET_RATOR" |
|
105 |
"LET_RAND" > "HOL4Base.bool.LET_RAND" |
|
106 |
"LET_DEF" > "HOL4Compat.LET_def" |
|
107 |
"LET_CONG" > "Recdef.let_cong" |
|
108 |
"LEFT_OR_OVER_AND" > "HOL.disj_conj_distribL" |
|
109 |
"LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3" |
|
110 |
"LEFT_FORALL_OR_THM" > "HOL.all_simps_3" |
|
17652 | 111 |
"LEFT_FORALL_IMP_THM" > "HOL.imp_ex" |
14516 | 112 |
"LEFT_EXISTS_IMP_THM" > "HOL.imp_all" |
113 |
"LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1" |
|
114 |
"LEFT_AND_OVER_OR" > "HOL.conj_disj_distribL" |
|
17652 | 115 |
"LEFT_AND_FORALL_THM" > "HOL.all_simps_1" |
14516 | 116 |
"IN_def" > "HOL4Base.bool.IN_def" |
117 |
"IN_DEF" > "HOL4Base.bool.IN_DEF" |
|
118 |
"INFINITY_AX" > "HOL4Setup.INFINITY_AX" |
|
119 |
"IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F" |
|
120 |
"IMP_F" > "HOL.notI" |
|
121 |
"IMP_DISJ_THM" > "Inductive.basic_monos_11" |
|
122 |
"IMP_CONG" > "HOL.imp_cong" |
|
123 |
"IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES" |
|
124 |
"IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as" |
|
125 |
"F_IMP" > "HOL4Base.bool.F_IMP" |
|
126 |
"F_DEF" > "HOL.False_def" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
127 |
"FUN_EQ_THM" > "Fun.fun_eq_iff" |
14516 | 128 |
"FORALL_THM" > "HOL4Base.bool.FORALL_THM" |
129 |
"FORALL_SIMP" > "HOL.simp_thms_35" |
|
130 |
"FORALL_DEF" > "HOL.All_def" |
|
131 |
"FORALL_AND_THM" > "HOL.all_conj_distrib" |
|
132 |
"FALSITY" > "HOL.FalseE" |
|
133 |
"EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF" |
|
134 |
"EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1" |
|
135 |
"EXISTS_UNIQUE_DEF" > "HOL4Compat.EXISTS_UNIQUE_DEF" |
|
136 |
"EXISTS_THM" > "HOL4Base.bool.EXISTS_THM" |
|
137 |
"EXISTS_SIMP" > "HOL.simp_thms_36" |
|
138 |
"EXISTS_REFL" > "HOL.simp_thms_37" |
|
139 |
"EXISTS_OR_THM" > "HOL.ex_disj_distrib" |
|
140 |
"EXISTS_DEF" > "HOL4Setup.EXISTS_DEF" |
|
141 |
"EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE" |
|
17188 | 142 |
"ETA_THM" > "Presburger.fm_modd_pinf" |
143 |
"ETA_AX" > "Presburger.fm_modd_pinf" |
|
14516 | 144 |
"EQ_TRANS" > "Set.basic_trans_rules_31" |
145 |
"EQ_SYM_EQ" > "HOL.eq_sym_conv" |
|
146 |
"EQ_SYM" > "HOL.meta_eq_to_obj_eq" |
|
17188 | 147 |
"EQ_REFL" > "Presburger.fm_modd_pinf" |
14516 | 148 |
"EQ_IMP_THM" > "HOL.iff_conv_conj_imp" |
17652 | 149 |
"EQ_EXT" > "HOL.meta_eq_to_obj_eq" |
14516 | 150 |
"EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND" |
151 |
"EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES" |
|
152 |
"DISJ_SYM" > "HOL.disj_comms_1" |
|
153 |
"DISJ_IMP_THM" > "HOL.imp_disjL" |
|
154 |
"DISJ_COMM" > "HOL.disj_comms_1" |
|
17188 | 155 |
"DISJ_ASSOC" > "Recdef.tfl_disj_assoc" |
14516 | 156 |
"DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM" |
157 |
"CONJ_SYM" > "HOL.conj_comms_1" |
|
158 |
"CONJ_COMM" > "HOL.conj_comms_1" |
|
159 |
"CONJ_ASSOC" > "HOL.conj_assoc" |
|
160 |
"COND_RATOR" > "HOL4Base.bool.COND_RATOR" |
|
161 |
"COND_RAND" > "HOL.if_distrib" |
|
162 |
"COND_ID" > "HOL.if_cancel" |
|
163 |
"COND_EXPAND" > "HOL4Base.bool.COND_EXPAND" |
|
164 |
"COND_DEF" > "HOL4Compat.COND_DEF" |
|
165 |
"COND_CONG" > "HOL4Base.bool.COND_CONG" |
|
166 |
"COND_CLAUSES" > "HOL4Base.bool.COND_CLAUSES" |
|
167 |
"COND_ABS" > "HOL4Base.bool.COND_ABS" |
|
168 |
"BOTH_FORALL_OR_THM" > "HOL4Base.bool.BOTH_FORALL_OR_THM" |
|
169 |
"BOTH_FORALL_IMP_THM" > "HOL4Base.bool.BOTH_FORALL_IMP_THM" |
|
170 |
"BOTH_EXISTS_IMP_THM" > "HOL4Base.bool.BOTH_EXISTS_IMP_THM" |
|
171 |
"BOTH_EXISTS_AND_THM" > "HOL4Base.bool.BOTH_EXISTS_AND_THM" |
|
172 |
"BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT" |
|
173 |
"BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM" |
|
174 |
"BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT" |
|
15647 | 175 |
"BOOL_CASES_AX" > "Datatype.bool.nchotomy" |
17188 | 176 |
"BETA_THM" > "Presburger.fm_modd_pinf" |
14516 | 177 |
"ARB_def" > "HOL4Base.bool.ARB_def" |
178 |
"ARB_DEF" > "HOL4Base.bool.ARB_DEF" |
|
179 |
"AND_INTRO_THM" > "HOL.conjI" |
|
180 |
"AND_IMP_INTRO" > "HOL.imp_conjL" |
|
181 |
"AND_DEF" > "HOL.and_def" |
|
182 |
"AND_CONG" > "HOL4Base.bool.AND_CONG" |
|
183 |
"AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES" |
|
184 |
"AND2_THM" > "HOL.conjunct2" |
|
185 |
"AND1_THM" > "HOL.conjunct1" |
|
17188 | 186 |
"ABS_SIMP" > "Presburger.fm_modd_pinf" |
14516 | 187 |
"ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM" |
188 |
||
189 |
ignore_thms |
|
190 |
"UNBOUNDED_THM" |
|
191 |
"UNBOUNDED_DEF" |
|
192 |
"BOUNDED_THM" |
|
193 |
"BOUNDED_DEF" |
|
194 |
||
195 |
end |