27898
|
1 |
# $Id$
|
|
2 |
# Default interpretation of some Isabelle symbols
|
|
3 |
|
|
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
|
|
357 |
|