2 # Default interpretation of some Isabelle symbols
4 symbol: \<zero> code: 0x01d7ec
5 symbol: \<one> code: 0x01d7ed
6 symbol: \<two> code: 0x01d7ee
7 symbol: \<three> code: 0x01d7ef
8 symbol: \<four> code: 0x01d7f0
9 symbol: \<five> code: 0x01d7f1
10 symbol: \<six> code: 0x01d7f2
11 symbol: \<seven> code: 0x01d7f3
12 symbol: \<eight> code: 0x01d7f4
13 symbol: \<nine> code: 0x01d7f5
14 symbol: \<A> code: 0x01d49c
15 symbol: \<B> code: 0x00212c
16 symbol: \<C> code: 0x01d49e
17 symbol: \<D> code: 0x01d49f
18 symbol: \<E> code: 0x002130
19 symbol: \<F> code: 0x002131
20 symbol: \<G> code: 0x01d4a2
21 symbol: \<H> code: 0x00210b
22 symbol: \<I> code: 0x002110
23 symbol: \<J> code: 0x01d4a5
24 symbol: \<K> code: 0x01d4a6
25 symbol: \<L> code: 0x002112
26 symbol: \<M> code: 0x002133
27 symbol: \<N> code: 0x01d4a9
28 symbol: \<O> code: 0x01d4aa
29 symbol: \<P> code: 0x01d4ab
30 symbol: \<Q> code: 0x01d4ac
31 symbol: \<R> code: 0x00211b
32 symbol: \<S> code: 0x01d4ae
33 symbol: \<T> code: 0x01d4af
34 symbol: \<U> code: 0x01d4b0
35 symbol: \<V> code: 0x01d4b1
36 symbol: \<W> code: 0x01d4b2
37 symbol: \<X> code: 0x01d4b3
38 symbol: \<Y> code: 0x01d4b4
39 symbol: \<Z> code: 0x01d4b5
40 symbol: \<a> code: 0x01d5ba
41 symbol: \<b> code: 0x01d5bb
42 symbol: \<c> code: 0x01d5bc
43 symbol: \<d> code: 0x01d5bd
44 symbol: \<e> code: 0x01d5be
45 symbol: \<f> code: 0x01d5bf
46 symbol: \<g> code: 0x01d5c0
47 symbol: \<h> code: 0x01d5c1
48 symbol: \<i> code: 0x01d5c2
49 symbol: \<j> code: 0x01d5c3
50 symbol: \<k> code: 0x01d5c4
51 symbol: \<l> code: 0x01d5c5
52 symbol: \<m> code: 0x01d5c6
53 symbol: \<n> code: 0x01d5c7
54 symbol: \<o> code: 0x01d5c8
55 symbol: \<p> code: 0x01d5c9
56 symbol: \<q> code: 0x01d5ca
57 symbol: \<r> code: 0x01d5cb
58 symbol: \<s> code: 0x01d5cc
59 symbol: \<t> code: 0x01d5cd
60 symbol: \<u> code: 0x01d5ce
61 symbol: \<v> code: 0x01d5cf
62 symbol: \<w> code: 0x01d5d0
63 symbol: \<x> code: 0x01d5d1
64 symbol: \<y> code: 0x01d5d2
65 symbol: \<z> code: 0x01d5d3
66 symbol: \<AA> code: 0x01d504
67 symbol: \<BB> code: 0x01d505
68 symbol: \<CC> code: 0x00212d
69 symbol: \<DD> code: 0x01d507
70 symbol: \<EE> code: 0x01d508
71 symbol: \<FF> code: 0x01d509
72 symbol: \<GG> code: 0x01d50a
73 symbol: \<HH> code: 0x00210c
74 symbol: \<II> code: 0x002111
75 symbol: \<JJ> code: 0x01d50d
76 symbol: \<KK> code: 0x01d50e
77 symbol: \<LL> code: 0x01d50f
78 symbol: \<MM> code: 0x01d510
79 symbol: \<NN> code: 0x01d511
80 symbol: \<OO> code: 0x01d512
81 symbol: \<PP> code: 0x01d513
82 symbol: \<QQ> code: 0x01d514
83 symbol: \<RR> code: 0x00211c
84 symbol: \<SS> code: 0x01d516
85 symbol: \<TT> code: 0x01d517
86 symbol: \<UU> code: 0x01d518
87 symbol: \<VV> code: 0x01d519
88 symbol: \<WW> code: 0x01d51a
89 symbol: \<XX> code: 0x01d51b
90 symbol: \<YY> code: 0x01d51c
91 symbol: \<ZZ> code: 0x002128
92 symbol: \<aa> code: 0x01d51e
93 symbol: \<bb> code: 0x01d51f
94 symbol: \<cc> code: 0x01d520
95 symbol: \<dd> code: 0x01d521
96 symbol: \<ee> code: 0x01d522
97 symbol: \<ff> code: 0x01d523
98 symbol: \<gg> code: 0x01d524
99 symbol: \<hh> code: 0x01d525
100 symbol: \<ii> code: 0x01d526
101 symbol: \<jj> code: 0x01d527
102 symbol: \<kk> code: 0x01d528
103 symbol: \<ll> code: 0x01d529
104 symbol: \<mm> code: 0x01d52a
105 symbol: \<nn> code: 0x01d52b
106 symbol: \<oo> code: 0x01d52c
107 symbol: \<pp> code: 0x01d52d
108 symbol: \<qq> code: 0x01d52e
109 symbol: \<rr> code: 0x01d52f
110 symbol: \<ss> code: 0x01d530
111 symbol: \<tt> code: 0x01d531
112 symbol: \<uu> code: 0x01d532
113 symbol: \<vv> code: 0x01d533
114 symbol: \<ww> code: 0x01d534
115 symbol: \<xx> code: 0x01d535
116 symbol: \<yy> code: 0x01d536
117 symbol: \<zz> code: 0x01d537
118 symbol: \<alpha> code: 0x0003b1
119 symbol: \<beta> code: 0x0003b2
120 symbol: \<gamma> code: 0x0003b3
121 symbol: \<delta> code: 0x0003b4
122 symbol: \<epsilon> code: 0x0003b5
123 symbol: \<zeta> code: 0x0003b6
124 symbol: \<eta> code: 0x0003b7
125 symbol: \<theta> code: 0x0003b8
126 symbol: \<iota> code: 0x0003b9
127 symbol: \<kappa> code: 0x0003ba
128 symbol: \<lambda> code: 0x0003bb
129 symbol: \<mu> code: 0x0003bc
130 symbol: \<nu> code: 0x0003bd
131 symbol: \<xi> code: 0x0003be
132 symbol: \<pi> code: 0x0003c0
133 symbol: \<rho> code: 0x0003c1
134 symbol: \<sigma> code: 0x0003c3
135 symbol: \<tau> code: 0x0003c4
136 symbol: \<upsilon> code: 0x0003c5
137 symbol: \<phi> code: 0x0003c6
138 symbol: \<chi> code: 0x0003c7
139 symbol: \<psi> code: 0x0003c8
140 symbol: \<omega> code: 0x0003c9
141 symbol: \<Gamma> code: 0x000393
142 symbol: \<Delta> code: 0x000394
143 symbol: \<Theta> code: 0x000398
144 symbol: \<Lambda> code: 0x00039b
145 symbol: \<Xi> code: 0x00039e
146 symbol: \<Pi> code: 0x0003a0
147 symbol: \<Sigma> code: 0x0003a3
148 symbol: \<Upsilon> code: 0x0003a5
149 symbol: \<Phi> code: 0x0003a6
150 symbol: \<Psi> code: 0x0003a8
151 symbol: \<Omega> code: 0x0003a9
152 symbol: \<bool> code: 0x01d539
153 symbol: \<complex> code: 0x002102
154 symbol: \<nat> code: 0x002115
155 symbol: \<rat> code: 0x00211a
156 symbol: \<real> code: 0x00211d
157 symbol: \<int> code: 0x002124
158 symbol: \<leftarrow> code: 0x002190
159 symbol: \<longleftarrow> code: 0x0027f5
160 symbol: \<rightarrow> code: 0x002192
161 symbol: \<longrightarrow> code: 0x0027f6
162 symbol: \<Leftarrow> code: 0x0021d0
163 symbol: \<Longleftarrow> code: 0x0027f8
164 symbol: \<Rightarrow> code: 0x0021d2
165 symbol: \<Longrightarrow> code: 0x0027f9
166 symbol: \<leftrightarrow> code: 0x002194
167 symbol: \<longleftrightarrow> code: 0x0027f7
168 symbol: \<Leftrightarrow> code: 0x0021d4
169 symbol: \<Longleftrightarrow> code: 0x0027fa
170 symbol: \<mapsto> code: 0x0021a6
171 symbol: \<longmapsto> code: 0x0027fc
172 symbol: \<midarrow> code: 0x002500
173 symbol: \<Midarrow> code: 0x002550
174 symbol: \<hookleftarrow> code: 0x0021a9
175 symbol: \<hookrightarrow> code: 0x0021aa
176 symbol: \<leftharpoondown> code: 0x0021bd
177 symbol: \<rightharpoondown> code: 0x0021c1
178 symbol: \<leftharpoonup> code: 0x0021bc
179 symbol: \<rightharpoonup> code: 0x0021c0
180 symbol: \<rightleftharpoons> code: 0x0021cc
181 symbol: \<leadsto> code: 0x00219d
182 symbol: \<downharpoonleft> code: 0x0021c3
183 symbol: \<downharpoonright> code: 0x0021c2
184 symbol: \<upharpoonleft> code: 0x0021bf
185 symbol: \<upharpoonright> code: 0x0021be
186 symbol: \<restriction> code: 0x0021be
187 symbol: \<Colon> code: 0x002237
188 symbol: \<up> code: 0x002191
189 symbol: \<Up> code: 0x0021d1
190 symbol: \<down> code: 0x002193
191 symbol: \<Down> code: 0x0021d3
192 symbol: \<updown> code: 0x002195
193 symbol: \<Updown> code: 0x0021d5
194 symbol: \<langle> code: 0x0027e8
195 symbol: \<rangle> code: 0x0027e9
196 symbol: \<lceil> code: 0x002308
197 symbol: \<rceil> code: 0x002309
198 symbol: \<lfloor> code: 0x00230a
199 symbol: \<rfloor> code: 0x00230b
200 symbol: \<lparr> code: 0x002987
201 symbol: \<rparr> code: 0x002988
202 symbol: \<lbrakk> code: 0x0027e6
203 symbol: \<rbrakk> code: 0x0027e7
204 symbol: \<lbrace> code: 0x002983
205 symbol: \<rbrace> code: 0x002984
206 symbol: \<guillemotleft> code: 0x0000ab
207 symbol: \<guillemotright> code: 0x0000bb
208 symbol: \<bottom> code: 0x0022a5
209 symbol: \<top> code: 0x0022a4
210 symbol: \<and> code: 0x002227
211 symbol: \<And> code: 0x0022c0
212 symbol: \<or> code: 0x002228
213 symbol: \<Or> code: 0x0022c1
214 symbol: \<forall> code: 0x002200
215 symbol: \<exists> code: 0x002203
216 symbol: \<nexists> code: 0x002204
217 symbol: \<not> code: 0x0000ac
218 symbol: \<box> code: 0x0025a1
219 symbol: \<diamond> code: 0x0025c7
220 symbol: \<turnstile> code: 0x0022a2
221 symbol: \<Turnstile> code: 0x0022a8
222 symbol: \<tturnstile> code: 0x0022a9
223 symbol: \<TTurnstile> code: 0x0022ab
224 symbol: \<stileturn> code: 0x0022a3
225 symbol: \<surd> code: 0x00221a
226 symbol: \<le> code: 0x002264
227 symbol: \<ge> code: 0x002265
228 symbol: \<lless> code: 0x00226a
229 symbol: \<ggreater> code: 0x00226b
230 symbol: \<lesssim> code: 0x002272
231 symbol: \<greatersim> code: 0x002273
232 symbol: \<lessapprox> code: 0x002a85
233 symbol: \<greaterapprox> code: 0x002a86
234 symbol: \<in> code: 0x002208
235 symbol: \<notin> code: 0x002209
236 symbol: \<subset> code: 0x002282
237 symbol: \<supset> code: 0x002283
238 symbol: \<subseteq> code: 0x002286
239 symbol: \<supseteq> code: 0x002287
240 symbol: \<sqsubset> code: 0x00228f
241 symbol: \<sqsupset> code: 0x002290
242 symbol: \<sqsubseteq> code: 0x002291
243 symbol: \<sqsupseteq> code: 0x002292
244 symbol: \<inter> code: 0x002229
245 symbol: \<Inter> code: 0x0022c2
246 symbol: \<union> code: 0x00222a
247 symbol: \<Union> code: 0x0022c3
248 symbol: \<squnion> code: 0x002294
249 symbol: \<Squnion> code: 0x002a06
250 symbol: \<sqinter> code: 0x002293
251 symbol: \<Sqinter> code: 0x002a05
252 symbol: \<setminus> code: 0x002216
253 symbol: \<propto> code: 0x00221d
254 symbol: \<uplus> code: 0x00228e
255 symbol: \<Uplus> code: 0x002a04
256 symbol: \<noteq> code: 0x002260
257 symbol: \<sim> code: 0x00223c
258 symbol: \<doteq> code: 0x002250
259 symbol: \<simeq> code: 0x002243
260 symbol: \<approx> code: 0x002248
261 symbol: \<asymp> code: 0x00224d
262 symbol: \<cong> code: 0x002245
263 symbol: \<smile> code: 0x002323
264 symbol: \<equiv> code: 0x002261
265 symbol: \<frown> code: 0x002322
266 symbol: \<Join> code: 0x0022c8
267 symbol: \<bowtie> code: 0x002a1d
268 symbol: \<prec> code: 0x00227a
269 symbol: \<succ> code: 0x00227b
270 symbol: \<preceq> code: 0x00227c
271 symbol: \<succeq> code: 0x00227d
272 symbol: \<parallel> code: 0x002225
273 symbol: \<bar> code: 0x0000a6
274 symbol: \<plusminus> code: 0x0000b1
275 symbol: \<minusplus> code: 0x002213
276 symbol: \<times> code: 0x0000d7
277 symbol: \<div> code: 0x0000f7
278 symbol: \<cdot> code: 0x0022c5
279 symbol: \<star> code: 0x0022c6
280 symbol: \<bullet> code: 0x002219
281 symbol: \<circ> code: 0x002218
282 symbol: \<dagger> code: 0x002020
283 symbol: \<ddagger> code: 0x002021
284 symbol: \<lhd> code: 0x0022b2
285 symbol: \<rhd> code: 0x0022b3
286 symbol: \<unlhd> code: 0x0022b4
287 symbol: \<unrhd> code: 0x0022b5
288 symbol: \<triangleleft> code: 0x0025c3
289 symbol: \<triangleright> code: 0x0025b9
290 symbol: \<triangle> code: 0x0025b3
291 symbol: \<triangleq> code: 0x00225c
292 symbol: \<oplus> code: 0x002295
293 symbol: \<Oplus> code: 0x002a01
294 symbol: \<otimes> code: 0x002297
295 symbol: \<Otimes> code: 0x002a02
296 symbol: \<odot> code: 0x002299
297 symbol: \<Odot> code: 0x002a00
298 symbol: \<ominus> code: 0x002296
299 symbol: \<oslash> code: 0x002298
300 symbol: \<dots> code: 0x002026
301 symbol: \<cdots> code: 0x0022ef
302 symbol: \<Sum> code: 0x002211
303 symbol: \<Prod> code: 0x00220f
304 symbol: \<Coprod> code: 0x002210
305 symbol: \<infinity> code: 0x00221e
306 symbol: \<integral> code: 0x00222b
307 symbol: \<ointegral> code: 0x00222e
308 symbol: \<clubsuit> code: 0x002663
309 symbol: \<diamondsuit> code: 0x002662
310 symbol: \<heartsuit> code: 0x002661
311 symbol: \<spadesuit> code: 0x002660
312 symbol: \<aleph> code: 0x002135
313 symbol: \<emptyset> code: 0x002205
314 symbol: \<nabla> code: 0x002207
315 symbol: \<partial> code: 0x002202
316 symbol: \<Re> code: 0x00211c
317 symbol: \<Im> code: 0x002111
318 symbol: \<flat> code: 0x00266d
319 symbol: \<natural> code: 0x00266e
320 symbol: \<sharp> code: 0x00266f
321 symbol: \<angle> code: 0x002220
322 symbol: \<copyright> code: 0x0000a9
323 symbol: \<registered> code: 0x0000ae
324 symbol: \<hyphen> code: 0x0000ad
325 symbol: \<inverse> code: 0x0000af
326 symbol: \<onesuperior> code: 0x0000b9
327 symbol: \<onequarter> code: 0x0000bc
328 symbol: \<twosuperior> code: 0x0000b2
329 symbol: \<onehalf> code: 0x0000bd
330 symbol: \<threesuperior> code: 0x0000b3
331 symbol: \<threequarters> code: 0x0000be
332 symbol: \<ordfeminine> code: 0x0000aa
333 symbol: \<ordmasculine> code: 0x0000ba
334 symbol: \<section> code: 0x0000a7
335 symbol: \<paragraph> code: 0x0000b6
336 symbol: \<exclamdown> code: 0x0000a1
337 symbol: \<questiondown> code: 0x0000bf
338 symbol: \<euro> code: 0x0020ac
339 symbol: \<pounds> code: 0x0000a3
340 symbol: \<yen> code: 0x0000a5
341 symbol: \<cent> code: 0x0000a2
342 symbol: \<currency> code: 0x0000a4
343 symbol: \<degree> code: 0x0000b0
344 symbol: \<amalg> code: 0x002a3f
345 symbol: \<mho> code: 0x002127
346 symbol: \<lozenge> code: 0x0025ca
347 symbol: \<wp> code: 0x002118
348 symbol: \<wrong> code: 0x002240
349 symbol: \<struct> code: 0x0022c4
350 symbol: \<acute> code: 0x0000b4
351 symbol: \<index> code: 0x000131
352 symbol: \<dieresis> code: 0x0000a8
353 symbol: \<cedilla> code: 0x0000b8
354 symbol: \<hungarumlaut> code: 0x0002dd
355 symbol: \<spacespace> code: 0x002423
356 symbol: \<some> code: 0x0003f5