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