author | haftmann |
Fri, 06 Jan 2012 10:19:49 +0100 | |
changeset 46133 | d9fe85d3d2cd |
parent 44763 | b50d5d694838 |
permissions | -rw-r--r-- |
14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"UNZIP_SND" > "UNZIP_SND_def" |
|
7 |
"UNZIP_FST" > "UNZIP_FST_def" |
|
8 |
"SUFFIX" > "SUFFIX_def" |
|
9 |
"SPLITP" > "SPLITP_def" |
|
10 |
"SNOC" > "SNOC_def" |
|
11 |
"SEG" > "SEG_def" |
|
12 |
"SCANR" > "SCANR_def" |
|
13 |
"SCANL" > "SCANL_def" |
|
14 |
"REPLICATE" > "REPLICATE_def" |
|
15 |
"PREFIX" > "PREFIX_def" |
|
16 |
"OR_EL" > "OR_EL_def" |
|
17 |
"LASTN" > "LASTN_def" |
|
18 |
"IS_SUFFIX" > "IS_SUFFIX_def" |
|
19 |
"IS_SUBLIST" > "IS_SUBLIST_def" |
|
20 |
"IS_PREFIX" > "IS_PREFIX_def" |
|
21 |
"GENLIST" > "GENLIST_def" |
|
22 |
"FIRSTN" > "FIRSTN_def" |
|
23 |
"ELL" > "ELL_def" |
|
24 |
"BUTLASTN" > "BUTLASTN_def" |
|
25 |
"BUTFIRSTN" > "BUTFIRSTN_def" |
|
26 |
"AND_EL" > "AND_EL_def" |
|
27 |
||
28 |
const_maps |
|
29 |
"UNZIP_SND" > "HOL4Base.rich_list.UNZIP_SND" |
|
30 |
"UNZIP_FST" > "HOL4Base.rich_list.UNZIP_FST" |
|
31 |
"SUFFIX" > "HOL4Base.rich_list.SUFFIX" |
|
32 |
"PREFIX" > "HOL4Base.rich_list.PREFIX" |
|
33 |
"OR_EL" > "HOL4Base.rich_list.OR_EL" |
|
34 |
"AND_EL" > "HOL4Base.rich_list.AND_EL" |
|
35 |
||
36 |
thm_maps |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
37 |
"list_INDUCT" > "HOL4Compat.list_INDUCT" |
14516 | 38 |
"list_CASES" > "HOL4Compat.list_CASES" |
39 |
"ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP" |
|
40 |
"ZIP_SNOC" > "HOL4Base.rich_list.ZIP_SNOC" |
|
41 |
"ZIP" > "HOL4Compat.ZIP" |
|
42 |
"UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP" |
|
43 |
"UNZIP_SNOC" > "HOL4Base.rich_list.UNZIP_SNOC" |
|
44 |
"UNZIP_SND_def" > "HOL4Base.rich_list.UNZIP_SND_def" |
|
45 |
"UNZIP_SND_DEF" > "HOL4Base.rich_list.UNZIP_SND_DEF" |
|
46 |
"UNZIP_FST_def" > "HOL4Base.rich_list.UNZIP_FST_def" |
|
47 |
"UNZIP_FST_DEF" > "HOL4Base.rich_list.UNZIP_FST_DEF" |
|
48 |
"UNZIP" > "HOL4Compat.UNZIP" |
|
49 |
"TL_SNOC" > "HOL4Base.rich_list.TL_SNOC" |
|
50 |
"TL" > "List.tl.simps_2" |
|
51 |
"SUM_SNOC" > "HOL4Base.rich_list.SUM_SNOC" |
|
52 |
"SUM_REVERSE" > "HOL4Base.rich_list.SUM_REVERSE" |
|
53 |
"SUM_FOLDR" > "HOL4Compat.sum_def" |
|
54 |
"SUM_FOLDL" > "HOL4Base.rich_list.SUM_FOLDL" |
|
55 |
"SUM_FLAT" > "HOL4Base.rich_list.SUM_FLAT" |
|
56 |
"SUM_APPEND" > "HOL4Base.rich_list.SUM_APPEND" |
|
57 |
"SUM" > "HOL4Compat.SUM" |
|
58 |
"SUFFIX_def" > "HOL4Base.rich_list.SUFFIX_def" |
|
59 |
"SUFFIX_DEF" > "HOL4Base.rich_list.SUFFIX_DEF" |
|
60 |
"SPLITP" > "HOL4Base.rich_list.SPLITP" |
|
61 |
"SOME_EL_SNOC" > "HOL4Base.rich_list.SOME_EL_SNOC" |
|
62 |
"SOME_EL_SEG" > "HOL4Base.rich_list.SOME_EL_SEG" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
63 |
"SOME_EL_REVERSE" > "List.list_ex_rev" |
14516 | 64 |
"SOME_EL_MAP" > "HOL4Base.rich_list.SOME_EL_MAP" |
65 |
"SOME_EL_LASTN" > "HOL4Base.rich_list.SOME_EL_LASTN" |
|
66 |
"SOME_EL_FOLDR_MAP" > "HOL4Base.rich_list.SOME_EL_FOLDR_MAP" |
|
67 |
"SOME_EL_FOLDR" > "HOL4Base.rich_list.SOME_EL_FOLDR" |
|
68 |
"SOME_EL_FOLDL_MAP" > "HOL4Base.rich_list.SOME_EL_FOLDL_MAP" |
|
69 |
"SOME_EL_FOLDL" > "HOL4Base.rich_list.SOME_EL_FOLDL" |
|
70 |
"SOME_EL_FIRSTN" > "HOL4Base.rich_list.SOME_EL_FIRSTN" |
|
71 |
"SOME_EL_DISJ" > "HOL4Base.rich_list.SOME_EL_DISJ" |
|
72 |
"SOME_EL_BUTLASTN" > "HOL4Base.rich_list.SOME_EL_BUTLASTN" |
|
73 |
"SOME_EL_BUTFIRSTN" > "HOL4Base.rich_list.SOME_EL_BUTFIRSTN" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
74 |
"SOME_EL_APPEND" > "List.list_ex_append" |
14516 | 75 |
"SOME_EL" > "HOL4Compat.list_exists_DEF" |
76 |
"SNOC_REVERSE_CONS" > "HOL4Base.rich_list.SNOC_REVERSE_CONS" |
|
77 |
"SNOC_INDUCT" > "HOL4Base.rich_list.SNOC_INDUCT" |
|
78 |
"SNOC_FOLDR" > "HOL4Base.rich_list.SNOC_FOLDR" |
|
79 |
"SNOC_EQ_LENGTH_EQ" > "HOL4Base.rich_list.SNOC_EQ_LENGTH_EQ" |
|
80 |
"SNOC_CASES" > "HOL4Base.rich_list.SNOC_CASES" |
|
81 |
"SNOC_Axiom" > "HOL4Base.rich_list.SNOC_Axiom" |
|
82 |
"SNOC_APPEND" > "HOL4Base.rich_list.SNOC_APPEND" |
|
83 |
"SNOC_11" > "HOL4Base.rich_list.SNOC_11" |
|
84 |
"SNOC" > "HOL4Base.rich_list.SNOC" |
|
85 |
"SEG_SUC_CONS" > "HOL4Base.rich_list.SEG_SUC_CONS" |
|
86 |
"SEG_SNOC" > "HOL4Base.rich_list.SEG_SNOC" |
|
87 |
"SEG_SEG" > "HOL4Base.rich_list.SEG_SEG" |
|
88 |
"SEG_REVERSE" > "HOL4Base.rich_list.SEG_REVERSE" |
|
89 |
"SEG_LENGTH_SNOC" > "HOL4Base.rich_list.SEG_LENGTH_SNOC" |
|
90 |
"SEG_LENGTH_ID" > "HOL4Base.rich_list.SEG_LENGTH_ID" |
|
91 |
"SEG_LASTN_BUTLASTN" > "HOL4Base.rich_list.SEG_LASTN_BUTLASTN" |
|
92 |
"SEG_FIRSTN_BUTFISTN" > "HOL4Base.rich_list.SEG_FIRSTN_BUTFISTN" |
|
93 |
"SEG_APPEND2" > "HOL4Base.rich_list.SEG_APPEND2" |
|
94 |
"SEG_APPEND1" > "HOL4Base.rich_list.SEG_APPEND1" |
|
95 |
"SEG_APPEND" > "HOL4Base.rich_list.SEG_APPEND" |
|
96 |
"SEG_0_SNOC" > "HOL4Base.rich_list.SEG_0_SNOC" |
|
97 |
"SEG" > "HOL4Base.rich_list.SEG" |
|
98 |
"SCANR" > "HOL4Base.rich_list.SCANR" |
|
99 |
"SCANL" > "HOL4Base.rich_list.SCANL" |
|
100 |
"REVERSE_SNOC" > "HOL4Base.rich_list.REVERSE_SNOC" |
|
101 |
"REVERSE_REVERSE" > "List.rev_rev_ident" |
|
102 |
"REVERSE_FOLDR" > "HOL4Base.rich_list.REVERSE_FOLDR" |
|
103 |
"REVERSE_FLAT" > "HOL4Base.rich_list.REVERSE_FLAT" |
|
104 |
"REVERSE_EQ_NIL" > "List.rev_is_Nil_conv" |
|
105 |
"REVERSE_APPEND" > "List.rev_append" |
|
106 |
"REVERSE" > "HOL4Base.rich_list.REVERSE" |
|
107 |
"REPLICATE" > "HOL4Base.rich_list.REPLICATE" |
|
108 |
"PREFIX_def" > "HOL4Base.rich_list.PREFIX_def" |
|
109 |
"PREFIX_FOLDR" > "HOL4Base.rich_list.PREFIX_FOLDR" |
|
110 |
"PREFIX_DEF" > "HOL4Base.rich_list.PREFIX_DEF" |
|
111 |
"PREFIX" > "HOL4Base.rich_list.PREFIX" |
|
112 |
"OR_EL_def" > "HOL4Base.rich_list.OR_EL_def" |
|
113 |
"OR_EL_FOLDR" > "HOL4Base.rich_list.OR_EL_FOLDR" |
|
114 |
"OR_EL_FOLDL" > "HOL4Base.rich_list.OR_EL_FOLDL" |
|
115 |
"OR_EL_DEF" > "HOL4Base.rich_list.OR_EL_DEF" |
|
116 |
"NULL_FOLDR" > "HOL4Base.rich_list.NULL_FOLDR" |
|
117 |
"NULL_FOLDL" > "HOL4Base.rich_list.NULL_FOLDL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
118 |
"NULL_EQ_NIL" > "List.eq_Nil_null" |
14516 | 119 |
"NULL_DEF" > "HOL4Compat.NULL_DEF" |
120 |
"NULL" > "HOL4Base.list.NULL" |
|
121 |
"NOT_SOME_EL_ALL_EL" > "HOL4Base.list.NOT_EXISTS" |
|
122 |
"NOT_SNOC_NIL" > "HOL4Base.rich_list.NOT_SNOC_NIL" |
|
123 |
"NOT_NIL_SNOC" > "HOL4Base.rich_list.NOT_NIL_SNOC" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
124 |
"NOT_NIL_CONS" > "List.list.distinct_1" |
14516 | 125 |
"NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
126 |
"NOT_CONS_NIL" > "List.list.distinct_2" |
14516 | 127 |
"NOT_ALL_EL_SOME_EL" > "HOL4Base.list.NOT_EVERY" |
128 |
"MONOID_APPEND_NIL" > "HOL4Base.rich_list.MONOID_APPEND_NIL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
129 |
"MAP_o" > "List.map.comp" |
14516 | 130 |
"MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC" |
131 |
"MAP_REVERSE" > "List.rev_map" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
132 |
"MAP_MAP_o" > "List.map.compositionality" |
14516 | 133 |
"MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR" |
134 |
"MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL" |
|
135 |
"MAP_FLAT" > "List.map_concat" |
|
136 |
"MAP_FILTER" > "HOL4Base.rich_list.MAP_FILTER" |
|
137 |
"MAP_APPEND" > "List.map_append" |
|
138 |
"MAP2_ZIP" > "HOL4Base.list.MAP2_ZIP" |
|
139 |
"MAP2" > "HOL4Compat.MAP2" |
|
140 |
"MAP" > "HOL4Compat.MAP" |
|
141 |
"LIST_NOT_EQ" > "HOL4Base.list.LIST_NOT_EQ" |
|
142 |
"LENGTH_ZIP" > "HOL4Base.list.LENGTH_ZIP" |
|
143 |
"LENGTH_UNZIP_SND" > "HOL4Base.rich_list.LENGTH_UNZIP_SND" |
|
144 |
"LENGTH_UNZIP_FST" > "HOL4Base.rich_list.LENGTH_UNZIP_FST" |
|
145 |
"LENGTH_SNOC" > "HOL4Base.rich_list.LENGTH_SNOC" |
|
146 |
"LENGTH_SEG" > "HOL4Base.rich_list.LENGTH_SEG" |
|
147 |
"LENGTH_SCANR" > "HOL4Base.rich_list.LENGTH_SCANR" |
|
148 |
"LENGTH_SCANL" > "HOL4Base.rich_list.LENGTH_SCANL" |
|
149 |
"LENGTH_REVERSE" > "List.length_rev" |
|
150 |
"LENGTH_REPLICATE" > "HOL4Base.rich_list.LENGTH_REPLICATE" |
|
151 |
"LENGTH_NOT_NULL" > "HOL4Base.rich_list.LENGTH_NOT_NULL" |
|
152 |
"LENGTH_NIL" > "List.length_0_conv" |
|
153 |
"LENGTH_MAP2" > "HOL4Base.rich_list.LENGTH_MAP2" |
|
154 |
"LENGTH_MAP" > "List.length_map" |
|
155 |
"LENGTH_LASTN" > "HOL4Base.rich_list.LENGTH_LASTN" |
|
156 |
"LENGTH_GENLIST" > "HOL4Base.rich_list.LENGTH_GENLIST" |
|
157 |
"LENGTH_FOLDR" > "HOL4Base.rich_list.LENGTH_FOLDR" |
|
158 |
"LENGTH_FOLDL" > "HOL4Base.rich_list.LENGTH_FOLDL" |
|
159 |
"LENGTH_FLAT" > "HOL4Base.rich_list.LENGTH_FLAT" |
|
160 |
"LENGTH_FIRSTN" > "HOL4Base.rich_list.LENGTH_FIRSTN" |
|
161 |
"LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL" |
|
162 |
"LENGTH_EQ" > "HOL4Base.rich_list.LENGTH_EQ" |
|
163 |
"LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS" |
|
164 |
"LENGTH_BUTLASTN" > "HOL4Base.rich_list.LENGTH_BUTLASTN" |
|
165 |
"LENGTH_BUTLAST" > "HOL4Base.rich_list.LENGTH_BUTLAST" |
|
166 |
"LENGTH_BUTFIRSTN" > "HOL4Base.rich_list.LENGTH_BUTFIRSTN" |
|
167 |
"LENGTH_APPEND" > "List.length_append" |
|
168 |
"LENGTH" > "HOL4Compat.LENGTH" |
|
169 |
"LAST_LASTN_LAST" > "HOL4Base.rich_list.LAST_LASTN_LAST" |
|
170 |
"LAST_CONS" > "HOL4Base.list.LAST_CONS" |
|
171 |
"LASTN_SEG" > "HOL4Base.rich_list.LASTN_SEG" |
|
172 |
"LASTN_REVERSE" > "HOL4Base.rich_list.LASTN_REVERSE" |
|
173 |
"LASTN_MAP" > "HOL4Base.rich_list.LASTN_MAP" |
|
174 |
"LASTN_LENGTH_ID" > "HOL4Base.rich_list.LASTN_LENGTH_ID" |
|
175 |
"LASTN_LENGTH_APPEND" > "HOL4Base.rich_list.LASTN_LENGTH_APPEND" |
|
176 |
"LASTN_LASTN" > "HOL4Base.rich_list.LASTN_LASTN" |
|
177 |
"LASTN_CONS" > "HOL4Base.rich_list.LASTN_CONS" |
|
178 |
"LASTN_BUTLASTN" > "HOL4Base.rich_list.LASTN_BUTLASTN" |
|
179 |
"LASTN_BUTFIRSTN" > "HOL4Base.rich_list.LASTN_BUTFIRSTN" |
|
180 |
"LASTN_APPEND2" > "HOL4Base.rich_list.LASTN_APPEND2" |
|
181 |
"LASTN_APPEND1" > "HOL4Base.rich_list.LASTN_APPEND1" |
|
182 |
"LASTN_1" > "HOL4Base.rich_list.LASTN_1" |
|
183 |
"LASTN" > "HOL4Base.rich_list.LASTN" |
|
184 |
"LAST" > "HOL4Base.rich_list.LAST" |
|
185 |
"IS_SUFFIX_REVERSE" > "HOL4Base.rich_list.IS_SUFFIX_REVERSE" |
|
186 |
"IS_SUFFIX_IS_SUBLIST" > "HOL4Base.rich_list.IS_SUFFIX_IS_SUBLIST" |
|
187 |
"IS_SUFFIX_APPEND" > "HOL4Base.rich_list.IS_SUFFIX_APPEND" |
|
188 |
"IS_SUFFIX" > "HOL4Base.rich_list.IS_SUFFIX" |
|
189 |
"IS_SUBLIST_REVERSE" > "HOL4Base.rich_list.IS_SUBLIST_REVERSE" |
|
190 |
"IS_SUBLIST_APPEND" > "HOL4Base.rich_list.IS_SUBLIST_APPEND" |
|
191 |
"IS_SUBLIST" > "HOL4Base.rich_list.IS_SUBLIST" |
|
192 |
"IS_PREFIX_REVERSE" > "HOL4Base.rich_list.IS_PREFIX_REVERSE" |
|
193 |
"IS_PREFIX_PREFIX" > "HOL4Base.rich_list.IS_PREFIX_PREFIX" |
|
194 |
"IS_PREFIX_IS_SUBLIST" > "HOL4Base.rich_list.IS_PREFIX_IS_SUBLIST" |
|
195 |
"IS_PREFIX_APPEND" > "HOL4Base.rich_list.IS_PREFIX_APPEND" |
|
196 |
"IS_PREFIX" > "HOL4Base.rich_list.IS_PREFIX" |
|
197 |
"IS_EL_SOME_EL" > "HOL4Base.rich_list.IS_EL_SOME_EL" |
|
198 |
"IS_EL_SNOC" > "HOL4Base.rich_list.IS_EL_SNOC" |
|
199 |
"IS_EL_SEG" > "HOL4Base.rich_list.IS_EL_SEG" |
|
200 |
"IS_EL_REVERSE" > "HOL4Base.rich_list.IS_EL_REVERSE" |
|
201 |
"IS_EL_REPLICATE" > "HOL4Base.rich_list.IS_EL_REPLICATE" |
|
202 |
"IS_EL_LASTN" > "HOL4Base.rich_list.IS_EL_LASTN" |
|
203 |
"IS_EL_FOLDR_MAP" > "HOL4Base.rich_list.IS_EL_FOLDR_MAP" |
|
204 |
"IS_EL_FOLDR" > "HOL4Base.rich_list.IS_EL_FOLDR" |
|
205 |
"IS_EL_FOLDL_MAP" > "HOL4Base.rich_list.IS_EL_FOLDL_MAP" |
|
206 |
"IS_EL_FOLDL" > "HOL4Base.rich_list.IS_EL_FOLDL" |
|
207 |
"IS_EL_FIRSTN" > "HOL4Base.rich_list.IS_EL_FIRSTN" |
|
208 |
"IS_EL_FILTER" > "HOL4Base.rich_list.IS_EL_FILTER" |
|
209 |
"IS_EL_DEF" > "HOL4Base.rich_list.IS_EL_DEF" |
|
210 |
"IS_EL_BUTLASTN" > "HOL4Base.rich_list.IS_EL_BUTLASTN" |
|
211 |
"IS_EL_BUTFIRSTN" > "HOL4Base.rich_list.IS_EL_BUTFIRSTN" |
|
212 |
"IS_EL_APPEND" > "HOL4Base.list.MEM_APPEND" |
|
213 |
"IS_EL" > "HOL4Compat.MEM" |
|
214 |
"HD" > "List.hd.simps" |
|
215 |
"GENLIST" > "HOL4Base.rich_list.GENLIST" |
|
216 |
"FOLDR_SNOC" > "HOL4Base.rich_list.FOLDR_SNOC" |
|
217 |
"FOLDR_SINGLE" > "HOL4Base.rich_list.FOLDR_SINGLE" |
|
218 |
"FOLDR_REVERSE" > "HOL4Base.rich_list.FOLDR_REVERSE" |
|
219 |
"FOLDR_MAP_REVERSE" > "HOL4Base.rich_list.FOLDR_MAP_REVERSE" |
|
220 |
"FOLDR_MAP" > "HOL4Base.rich_list.FOLDR_MAP" |
|
221 |
"FOLDR_FOLDL_REVERSE" > "List.foldr_foldl" |
|
222 |
"FOLDR_FOLDL" > "HOL4Base.rich_list.FOLDR_FOLDL" |
|
223 |
"FOLDR_FILTER_REVERSE" > "HOL4Base.rich_list.FOLDR_FILTER_REVERSE" |
|
224 |
"FOLDR_FILTER" > "HOL4Base.rich_list.FOLDR_FILTER" |
|
225 |
"FOLDR_CONS_NIL" > "HOL4Base.rich_list.FOLDR_CONS_NIL" |
|
226 |
"FOLDR_APPEND" > "List.foldr_append" |
|
227 |
"FOLDR" > "HOL4Compat.FOLDR" |
|
228 |
"FOLDL_SNOC_NIL" > "HOL4Base.rich_list.FOLDL_SNOC_NIL" |
|
229 |
"FOLDL_SNOC" > "HOL4Base.rich_list.FOLDL_SNOC" |
|
230 |
"FOLDL_SINGLE" > "HOL4Base.rich_list.FOLDL_SINGLE" |
|
231 |
"FOLDL_REVERSE" > "HOL4Base.rich_list.FOLDL_REVERSE" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
232 |
"FOLDL_MAP" > "List.foldl_map" |
14516 | 233 |
"FOLDL_FOLDR_REVERSE" > "List.foldl_foldr" |
234 |
"FOLDL_FILTER" > "HOL4Base.rich_list.FOLDL_FILTER" |
|
235 |
"FOLDL_APPEND" > "List.foldl_append" |
|
236 |
"FOLDL" > "HOL4Compat.FOLDL" |
|
237 |
"FLAT_SNOC" > "HOL4Base.rich_list.FLAT_SNOC" |
|
238 |
"FLAT_REVERSE" > "HOL4Base.rich_list.FLAT_REVERSE" |
|
239 |
"FLAT_FOLDR" > "HOL4Base.rich_list.FLAT_FOLDR" |
|
240 |
"FLAT_FLAT" > "HOL4Base.rich_list.FLAT_FLAT" |
|
241 |
"FLAT_APPEND" > "List.concat_append" |
|
242 |
"FLAT" > "HOL4Compat.FLAT" |
|
243 |
"FIRSTN_SNOC" > "HOL4Base.rich_list.FIRSTN_SNOC" |
|
244 |
"FIRSTN_SEG" > "HOL4Base.rich_list.FIRSTN_SEG" |
|
245 |
"FIRSTN_REVERSE" > "HOL4Base.rich_list.FIRSTN_REVERSE" |
|
246 |
"FIRSTN_LENGTH_ID" > "HOL4Base.rich_list.FIRSTN_LENGTH_ID" |
|
247 |
"FIRSTN_LENGTH_APPEND" > "HOL4Base.rich_list.FIRSTN_LENGTH_APPEND" |
|
248 |
"FIRSTN_FIRSTN" > "HOL4Base.rich_list.FIRSTN_FIRSTN" |
|
249 |
"FIRSTN_BUTLASTN" > "HOL4Base.rich_list.FIRSTN_BUTLASTN" |
|
250 |
"FIRSTN_APPEND2" > "HOL4Base.rich_list.FIRSTN_APPEND2" |
|
251 |
"FIRSTN_APPEND1" > "HOL4Base.rich_list.FIRSTN_APPEND1" |
|
252 |
"FIRSTN" > "HOL4Base.rich_list.FIRSTN" |
|
253 |
"FILTER_SNOC" > "HOL4Base.rich_list.FILTER_SNOC" |
|
15647 | 254 |
"FILTER_REVERSE" > "List.rev_filter" |
17188 | 255 |
"FILTER_MAP" > "List.filter_map" |
14516 | 256 |
"FILTER_IDEM" > "HOL4Base.rich_list.FILTER_IDEM" |
257 |
"FILTER_FOLDR" > "HOL4Base.rich_list.FILTER_FOLDR" |
|
258 |
"FILTER_FOLDL" > "HOL4Base.rich_list.FILTER_FOLDL" |
|
259 |
"FILTER_FLAT" > "List.filter_concat" |
|
260 |
"FILTER_FILTER" > "HOL4Base.rich_list.FILTER_FILTER" |
|
261 |
"FILTER_COMM" > "HOL4Base.rich_list.FILTER_COMM" |
|
262 |
"FILTER_APPEND" > "List.filter_append" |
|
263 |
"FILTER" > "HOL4Compat.FILTER" |
|
264 |
"FCOMM_FOLDR_FLAT" > "HOL4Base.rich_list.FCOMM_FOLDR_FLAT" |
|
265 |
"FCOMM_FOLDR_APPEND" > "HOL4Base.rich_list.FCOMM_FOLDR_APPEND" |
|
266 |
"FCOMM_FOLDL_FLAT" > "HOL4Base.rich_list.FCOMM_FOLDL_FLAT" |
|
267 |
"FCOMM_FOLDL_APPEND" > "HOL4Base.rich_list.FCOMM_FOLDL_APPEND" |
|
268 |
"EQ_LIST" > "HOL4Base.list.EQ_LIST" |
|
269 |
"EL_SNOC" > "HOL4Base.rich_list.EL_SNOC" |
|
270 |
"EL_SEG" > "HOL4Base.rich_list.EL_SEG" |
|
271 |
"EL_REVERSE_ELL" > "HOL4Base.rich_list.EL_REVERSE_ELL" |
|
272 |
"EL_REVERSE" > "HOL4Base.rich_list.EL_REVERSE" |
|
273 |
"EL_PRE_LENGTH" > "HOL4Base.rich_list.EL_PRE_LENGTH" |
|
274 |
"EL_MAP" > "HOL4Base.rich_list.EL_MAP" |
|
275 |
"EL_LENGTH_SNOC" > "HOL4Base.rich_list.EL_LENGTH_SNOC" |
|
276 |
"EL_LENGTH_APPEND" > "HOL4Base.rich_list.EL_LENGTH_APPEND" |
|
277 |
"EL_IS_EL" > "HOL4Base.rich_list.EL_IS_EL" |
|
278 |
"EL_ELL" > "HOL4Base.rich_list.EL_ELL" |
|
279 |
"EL_CONS" > "HOL4Base.rich_list.EL_CONS" |
|
280 |
"EL_APPEND2" > "HOL4Base.rich_list.EL_APPEND2" |
|
281 |
"EL_APPEND1" > "HOL4Base.rich_list.EL_APPEND1" |
|
282 |
"ELL_SUC_SNOC" > "HOL4Base.rich_list.ELL_SUC_SNOC" |
|
283 |
"ELL_SNOC" > "HOL4Base.rich_list.ELL_SNOC" |
|
284 |
"ELL_SEG" > "HOL4Base.rich_list.ELL_SEG" |
|
285 |
"ELL_REVERSE_EL" > "HOL4Base.rich_list.ELL_REVERSE_EL" |
|
286 |
"ELL_REVERSE" > "HOL4Base.rich_list.ELL_REVERSE" |
|
287 |
"ELL_PRE_LENGTH" > "HOL4Base.rich_list.ELL_PRE_LENGTH" |
|
288 |
"ELL_MAP" > "HOL4Base.rich_list.ELL_MAP" |
|
289 |
"ELL_LENGTH_SNOC" > "HOL4Base.rich_list.ELL_LENGTH_SNOC" |
|
290 |
"ELL_LENGTH_CONS" > "HOL4Base.rich_list.ELL_LENGTH_CONS" |
|
291 |
"ELL_LENGTH_APPEND" > "HOL4Base.rich_list.ELL_LENGTH_APPEND" |
|
292 |
"ELL_LAST" > "HOL4Base.rich_list.ELL_LAST" |
|
293 |
"ELL_IS_EL" > "HOL4Base.rich_list.ELL_IS_EL" |
|
294 |
"ELL_EL" > "HOL4Base.rich_list.ELL_EL" |
|
295 |
"ELL_CONS" > "HOL4Base.rich_list.ELL_CONS" |
|
296 |
"ELL_APPEND2" > "HOL4Base.rich_list.ELL_APPEND2" |
|
297 |
"ELL_APPEND1" > "HOL4Base.rich_list.ELL_APPEND1" |
|
298 |
"ELL_0_SNOC" > "HOL4Base.rich_list.ELL_0_SNOC" |
|
299 |
"ELL" > "HOL4Base.rich_list.ELL" |
|
300 |
"EL" > "HOL4Base.rich_list.EL" |
|
301 |
"CONS_APPEND" > "HOL4Base.rich_list.CONS_APPEND" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
33640
diff
changeset
|
302 |
"CONS_11" > "List.list.inject" |
14516 | 303 |
"CONS" > "HOL4Base.list.CONS" |
304 |
"COMM_MONOID_FOLDR" > "HOL4Base.rich_list.COMM_MONOID_FOLDR" |
|
305 |
"COMM_MONOID_FOLDL" > "HOL4Base.rich_list.COMM_MONOID_FOLDL" |
|
306 |
"COMM_ASSOC_FOLDR_REVERSE" > "HOL4Base.rich_list.COMM_ASSOC_FOLDR_REVERSE" |
|
307 |
"COMM_ASSOC_FOLDL_REVERSE" > "HOL4Base.rich_list.COMM_ASSOC_FOLDL_REVERSE" |
|
308 |
"BUTLAST_CONS" > "HOL4Base.list.FRONT_CONS" |
|
309 |
"BUTLASTN_SUC_BUTLAST" > "HOL4Base.rich_list.BUTLASTN_SUC_BUTLAST" |
|
310 |
"BUTLASTN_SEG" > "HOL4Base.rich_list.BUTLASTN_SEG" |
|
311 |
"BUTLASTN_REVERSE" > "HOL4Base.rich_list.BUTLASTN_REVERSE" |
|
312 |
"BUTLASTN_MAP" > "HOL4Base.rich_list.BUTLASTN_MAP" |
|
313 |
"BUTLASTN_LENGTH_NIL" > "HOL4Base.rich_list.BUTLASTN_LENGTH_NIL" |
|
314 |
"BUTLASTN_LENGTH_CONS" > "HOL4Base.rich_list.BUTLASTN_LENGTH_CONS" |
|
315 |
"BUTLASTN_LENGTH_APPEND" > "HOL4Base.rich_list.BUTLASTN_LENGTH_APPEND" |
|
316 |
"BUTLASTN_LASTN_NIL" > "HOL4Base.rich_list.BUTLASTN_LASTN_NIL" |
|
317 |
"BUTLASTN_LASTN" > "HOL4Base.rich_list.BUTLASTN_LASTN" |
|
318 |
"BUTLASTN_FIRSTN" > "HOL4Base.rich_list.BUTLASTN_FIRSTN" |
|
319 |
"BUTLASTN_CONS" > "HOL4Base.rich_list.BUTLASTN_CONS" |
|
320 |
"BUTLASTN_BUTLASTN" > "HOL4Base.rich_list.BUTLASTN_BUTLASTN" |
|
321 |
"BUTLASTN_BUTLAST" > "HOL4Base.rich_list.BUTLASTN_BUTLAST" |
|
322 |
"BUTLASTN_APPEND2" > "HOL4Base.rich_list.BUTLASTN_APPEND2" |
|
323 |
"BUTLASTN_APPEND1" > "HOL4Base.rich_list.BUTLASTN_APPEND1" |
|
324 |
"BUTLASTN_1" > "HOL4Base.rich_list.BUTLASTN_1" |
|
325 |
"BUTLASTN" > "HOL4Base.rich_list.BUTLASTN" |
|
326 |
"BUTLAST" > "HOL4Base.rich_list.BUTLAST" |
|
327 |
"BUTFIRSTN_SNOC" > "HOL4Base.rich_list.BUTFIRSTN_SNOC" |
|
328 |
"BUTFIRSTN_SEG" > "HOL4Base.rich_list.BUTFIRSTN_SEG" |
|
329 |
"BUTFIRSTN_REVERSE" > "HOL4Base.rich_list.BUTFIRSTN_REVERSE" |
|
330 |
"BUTFIRSTN_LENGTH_NIL" > "HOL4Base.rich_list.BUTFIRSTN_LENGTH_NIL" |
|
331 |
"BUTFIRSTN_LENGTH_APPEND" > "HOL4Base.rich_list.BUTFIRSTN_LENGTH_APPEND" |
|
332 |
"BUTFIRSTN_LASTN" > "HOL4Base.rich_list.BUTFIRSTN_LASTN" |
|
333 |
"BUTFIRSTN_BUTFIRSTN" > "HOL4Base.rich_list.BUTFIRSTN_BUTFIRSTN" |
|
334 |
"BUTFIRSTN_APPEND2" > "HOL4Base.rich_list.BUTFIRSTN_APPEND2" |
|
335 |
"BUTFIRSTN_APPEND1" > "HOL4Base.rich_list.BUTFIRSTN_APPEND1" |
|
336 |
"BUTFIRSTN" > "HOL4Base.rich_list.BUTFIRSTN" |
|
337 |
"ASSOC_FOLDR_FLAT" > "HOL4Base.rich_list.ASSOC_FOLDR_FLAT" |
|
338 |
"ASSOC_FOLDL_FLAT" > "HOL4Base.rich_list.ASSOC_FOLDL_FLAT" |
|
339 |
"ASSOC_APPEND" > "HOL4Base.rich_list.ASSOC_APPEND" |
|
340 |
"APPEND_SNOC" > "HOL4Base.rich_list.APPEND_SNOC" |
|
341 |
"APPEND_NIL" > "HOL4Base.rich_list.APPEND_NIL" |
|
342 |
"APPEND_LENGTH_EQ" > "HOL4Base.rich_list.APPEND_LENGTH_EQ" |
|
343 |
"APPEND_FOLDR" > "HOL4Base.rich_list.APPEND_FOLDR" |
|
344 |
"APPEND_FOLDL" > "HOL4Base.rich_list.APPEND_FOLDL" |
|
345 |
"APPEND_FIRSTN_LASTN" > "HOL4Base.rich_list.APPEND_FIRSTN_LASTN" |
|
346 |
"APPEND_FIRSTN_BUTFIRSTN" > "HOL4Base.rich_list.APPEND_FIRSTN_BUTFIRSTN" |
|
347 |
"APPEND_BUTLAST_LAST" > "List.append_butlast_last_id" |
|
348 |
"APPEND_BUTLASTN_LASTN" > "HOL4Base.rich_list.APPEND_BUTLASTN_LASTN" |
|
349 |
"APPEND_BUTLASTN_BUTFIRSTN" > "HOL4Base.rich_list.APPEND_BUTLASTN_BUTFIRSTN" |
|
350 |
"APPEND_ASSOC" > "List.append_assoc" |
|
351 |
"APPEND" > "HOL4Compat.APPEND" |
|
352 |
"AND_EL_def" > "HOL4Base.rich_list.AND_EL_def" |
|
353 |
"AND_EL_FOLDR" > "HOL4Base.rich_list.AND_EL_FOLDR" |
|
354 |
"AND_EL_FOLDL" > "HOL4Base.rich_list.AND_EL_FOLDL" |
|
355 |
"AND_EL_DEF" > "HOL4Base.rich_list.AND_EL_DEF" |
|
356 |
"ALL_EL_SNOC" > "HOL4Base.rich_list.ALL_EL_SNOC" |
|
357 |
"ALL_EL_SEG" > "HOL4Base.rich_list.ALL_EL_SEG" |
|
15647 | 358 |
"ALL_EL_REVERSE" > "List.list_all_rev" |
14516 | 359 |
"ALL_EL_REPLICATE" > "HOL4Base.rich_list.ALL_EL_REPLICATE" |
360 |
"ALL_EL_MAP" > "HOL4Base.rich_list.ALL_EL_MAP" |
|
361 |
"ALL_EL_LASTN" > "HOL4Base.rich_list.ALL_EL_LASTN" |
|
362 |
"ALL_EL_FOLDR_MAP" > "HOL4Base.rich_list.ALL_EL_FOLDR_MAP" |
|
363 |
"ALL_EL_FOLDR" > "HOL4Base.rich_list.ALL_EL_FOLDR" |
|
364 |
"ALL_EL_FOLDL_MAP" > "HOL4Base.rich_list.ALL_EL_FOLDL_MAP" |
|
365 |
"ALL_EL_FOLDL" > "HOL4Base.rich_list.ALL_EL_FOLDL" |
|
366 |
"ALL_EL_FIRSTN" > "HOL4Base.rich_list.ALL_EL_FIRSTN" |
|
367 |
"ALL_EL_CONJ" > "HOL4Base.list.EVERY_CONJ" |
|
368 |
"ALL_EL_BUTLASTN" > "HOL4Base.rich_list.ALL_EL_BUTLASTN" |
|
369 |
"ALL_EL_BUTFIRSTN" > "HOL4Base.rich_list.ALL_EL_BUTFIRSTN" |
|
370 |
"ALL_EL_APPEND" > "List.list_all_append" |
|
371 |
"ALL_EL" > "HOL4Compat.EVERY_DEF" |
|
372 |
||
373 |
end |