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 \<rightarrow> code: 0x002192 group: arrow abbrev: .> abbrev: ->
160 \<longrightarrow> code: 0x0027f6 group: arrow abbrev: .> abbrev: -->
161 \<Leftarrow> code: 0x0021d0 group: arrow abbrev: <.
162 \<Longleftarrow> code: 0x0027f8 group: arrow abbrev: <.
163 \<Rightarrow> code: 0x0021d2 group: arrow abbrev: .> abbrev: =>
164 \<Longrightarrow> code: 0x0027f9 group: arrow abbrev: .> abbrev: ==>
165 \<leftrightarrow> code: 0x002194 group: arrow abbrev: <> abbrev: <->
166 \<longleftrightarrow> code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <-->
167 \<Leftrightarrow> code: 0x0021d4 group: arrow abbrev: <>
168 \<Longleftrightarrow> code: 0x0027fa group: arrow abbrev: <>
169 \<mapsto> code: 0x0021a6 group: arrow abbrev: .> abbrev: |->
170 \<longmapsto> code: 0x0027fc group: arrow abbrev: .> abbrev: |-->
171 \<midarrow> code: 0x002500 group: arrow abbrev: <>
172 \<Midarrow> code: 0x002550 group: arrow abbrev: <>
173 \<hookleftarrow> code: 0x0021a9 group: arrow abbrev: <.
174 \<hookrightarrow> code: 0x0021aa group: arrow abbrev: .>
175 \<leftharpoondown> code: 0x0021bd group: arrow abbrev: <.
176 \<rightharpoondown> code: 0x0021c1 group: arrow abbrev: .>
177 \<leftharpoonup> code: 0x0021bc group: arrow abbrev: <.
178 \<rightharpoonup> code: 0x0021c0 group: arrow abbrev: .>
179 \<rightleftharpoons> code: 0x0021cc group: arrow abbrev: <> abbrev: ==
180 \<leadsto> code: 0x00219d group: arrow abbrev: .> abbrev: ~>
181 \<downharpoonleft> code: 0x0021c3 group: arrow
182 \<downharpoonright> code: 0x0021c2 group: arrow
183 \<upharpoonleft> code: 0x0021bf group: arrow
184 #\<upharpoonright> code: 0x0021be group: arrow
185 \<restriction> code: 0x0021be group: punctuation
186 \<Colon> code: 0x002237 group: punctuation
187 \<up> code: 0x002191 group: arrow
188 \<Up> code: 0x0021d1 group: arrow
189 \<down> code: 0x002193 group: arrow
190 \<Down> code: 0x0021d3 group: arrow
191 \<updown> code: 0x002195 group: arrow
192 \<Updown> code: 0x0021d5 group: arrow
193 \<langle> code: 0x0027e8 group: punctuation abbrev: <<
194 \<rangle> code: 0x0027e9 group: punctuation abbrev: >>
195 \<lceil> code: 0x002308 group: punctuation abbrev: [.
196 \<rceil> code: 0x002309 group: punctuation abbrev: .]
197 \<lfloor> code: 0x00230a group: punctuation abbrev: [.
198 \<rfloor> code: 0x00230b group: punctuation abbrev: .]
199 \<lparr> code: 0x002987 group: punctuation abbrev: (|
200 \<rparr> code: 0x002988 group: punctuation abbrev: |)
201 \<lbrakk> code: 0x0027e6 group: punctuation abbrev: [|
202 \<rbrakk> code: 0x0027e7 group: punctuation abbrev: |]
203 \<lbrace> code: 0x002983 group: punctuation abbrev: {|
204 \<rbrace> code: 0x002984 group: punctuation abbrev: |}
205 \<guillemotleft> code: 0x0000ab group: punctuation abbrev: <<
206 \<guillemotright> code: 0x0000bb group: punctuation abbrev: >>
207 \<bottom> code: 0x0022a5 group: logic
208 \<top> code: 0x0022a4 group: logic
209 \<and> code: 0x002227 group: logic abbrev: /\ abbrev: &
210 \<And> code: 0x0022c0 group: logic abbrev: !!
211 \<or> code: 0x002228 group: logic abbrev: \/ abbrev: |
212 \<Or> code: 0x0022c1 group: logic abbrev: ??
213 \<forall> code: 0x002200 group: logic abbrev: ! abbrev: ALL
214 \<exists> code: 0x002203 group: logic abbrev: ? abbrev: EX
215 \<nexists> code: 0x002204 group: logic abbrev: ~?
216 \<not> code: 0x0000ac group: logic abbrev: ~
217 \<box> code: 0x0025a1 group: logic
218 \<diamond> code: 0x0025c7 group: logic
219 \<turnstile> code: 0x0022a2 group: relation abbrev: |-
220 \<Turnstile> code: 0x0022a8 group: relation abbrev: |=
221 \<tturnstile> code: 0x0022a9 group: relation abbrev: |-
222 \<TTurnstile> code: 0x0022ab group: relation abbrev: |=
223 \<stileturn> code: 0x0022a3 group: relation abbrev: -|
224 \<surd> code: 0x00221a group: relation
225 \<le> code: 0x002264 group: relation abbrev: <=
226 \<ge> code: 0x002265 group: relation abbrev: >=
227 \<lless> code: 0x00226a group: relation abbrev: <<
228 \<ggreater> code: 0x00226b group: relation abbrev: >>
229 \<lesssim> code: 0x002272 group: relation
230 \<greatersim> code: 0x002273 group: relation
231 \<lessapprox> code: 0x002a85 group: relation
232 \<greaterapprox> code: 0x002a86 group: relation
233 \<in> code: 0x002208 group: relation abbrev: :
234 \<notin> code: 0x002209 group: relation abbrev: ~:
235 \<subset> code: 0x002282 group: relation
236 \<supset> code: 0x002283 group: relation
237 \<subseteq> code: 0x002286 group: relation abbrev: (=
238 \<supseteq> code: 0x002287 group: relation abbrev: )=
239 \<sqsubset> code: 0x00228f group: relation
240 \<sqsupset> code: 0x002290 group: relation
241 \<sqsubseteq> code: 0x002291 group: relation abbrev: [=
242 \<sqsupseteq> code: 0x002292 group: relation abbrev: ]=
243 \<inter> code: 0x002229 group: operator abbrev: Int
244 \<Inter> code: 0x0022c2 group: operator abbrev: Inter abbrev: INT
245 \<union> code: 0x00222a group: operator abbrev: Un
246 \<Union> code: 0x0022c3 group: operator abbrev: Union abbrev: UN
247 \<squnion> code: 0x002294 group: operator
248 \<Squnion> code: 0x002a06 group: operator abbrev: SUP
249 \<sqinter> code: 0x002293 group: operator
250 \<Sqinter> code: 0x002a05 group: operator abbrev: INF
251 \<setminus> code: 0x002216 group: operator
252 \<propto> code: 0x00221d group: operator
253 \<uplus> code: 0x00228e group: operator
254 \<Uplus> code: 0x002a04 group: operator
255 \<noteq> code: 0x002260 group: relation abbrev: ~=
256 \<sim> code: 0x00223c group: relation
257 \<doteq> code: 0x002250 group: relation abbrev: .=
258 \<simeq> code: 0x002243 group: relation
259 \<approx> code: 0x002248 group: relation
260 \<asymp> code: 0x00224d group: relation
261 \<cong> code: 0x002245 group: relation
262 \<smile> code: 0x002323 group: relation
263 \<equiv> code: 0x002261 group: relation abbrev: ==
264 \<frown> code: 0x002322 group: relation
265 \<Join> code: 0x0022c8
266 \<bowtie> code: 0x002a1d
267 \<prec> code: 0x00227a group: relation
268 \<succ> code: 0x00227b group: relation
269 \<preceq> code: 0x00227c group: relation
270 \<succeq> code: 0x00227d group: relation
271 \<parallel> code: 0x002225 group: punctuation abbrev: ||
272 \<bar> code: 0x0000a6 group: punctuation abbrev: ||
273 \<plusminus> code: 0x0000b1 group: operator
274 \<minusplus> code: 0x002213 group: operator
275 \<times> code: 0x0000d7 group: operator abbrev: <*>
276 \<div> code: 0x0000f7 group: operator
277 \<cdot> code: 0x0022c5 group: operator
278 \<star> code: 0x0022c6 group: operator
279 \<bullet> code: 0x002219 group: operator
280 \<circ> code: 0x002218 group: operator
281 \<dagger> code: 0x002020
282 \<ddagger> code: 0x002021
283 \<lhd> code: 0x0022b2 group: relation
284 \<rhd> code: 0x0022b3 group: relation
285 \<unlhd> code: 0x0022b4 group: relation
286 \<unrhd> code: 0x0022b5 group: relation
287 \<triangleleft> code: 0x0025c3 group: relation
288 \<triangleright> code: 0x0025b9 group: relation
289 \<triangle> code: 0x0025b3 group: relation
290 \<triangleq> code: 0x00225c group: relation
291 \<oplus> code: 0x002295 group: operator abbrev: +o
292 \<Oplus> code: 0x002a01 group: operator abbrev: +O
293 \<otimes> code: 0x002297 group: operator abbrev: *o
294 \<Otimes> code: 0x002a02 group: operator abbrev: *O
295 \<odot> code: 0x002299 group: operator abbrev: .o
296 \<Odot> code: 0x002a00 group: operator abbrev: .O
297 \<ominus> code: 0x002296 group: operator abbrev: -o
298 \<oslash> code: 0x002298 group: operator abbrev: /o
299 \<dots> code: 0x002026 group: punctuation abbrev: ...
300 \<cdots> code: 0x0022ef group: punctuation
301 \<Sum> code: 0x002211 group: operator abbrev: SUM
302 \<Prod> code: 0x00220f group: operator abbrev: PROD
303 \<Coprod> code: 0x002210 group: operator
304 \<infinity> code: 0x00221e
305 \<integral> code: 0x00222b group: operator
306 \<ointegral> code: 0x00222e group: operator
307 \<clubsuit> code: 0x002663
308 \<diamondsuit> code: 0x002662
309 \<heartsuit> code: 0x002661
310 \<spadesuit> code: 0x002660
311 \<aleph> code: 0x002135
312 \<emptyset> code: 0x002205
313 \<nabla> code: 0x002207
314 \<partial> code: 0x002202
315 \<flat> code: 0x00266d
316 \<natural> code: 0x00266e
317 \<sharp> code: 0x00266f
318 \<angle> code: 0x002220
319 \<copyright> code: 0x0000a9
320 \<registered> code: 0x0000ae
321 \<hyphen> code: 0x0000ad group: punctuation
322 \<inverse> code: 0x0000af group: punctuation
323 \<onequarter> code: 0x0000bc group: digit
324 \<onehalf> code: 0x0000bd group: digit
325 \<threequarters> code: 0x0000be group: digit
326 \<ordfeminine> code: 0x0000aa
327 \<ordmasculine> code: 0x0000ba
328 \<section> code: 0x0000a7
329 \<paragraph> code: 0x0000b6
330 \<exclamdown> code: 0x0000a1
331 \<questiondown> code: 0x0000bf
332 \<euro> code: 0x0020ac
333 \<pounds> code: 0x0000a3
334 \<yen> code: 0x0000a5
335 \<cent> code: 0x0000a2
336 \<currency> code: 0x0000a4
337 \<degree> code: 0x0000b0
338 \<amalg> code: 0x002a3f group: operator
339 \<mho> code: 0x002127 group: operator
340 \<lozenge> code: 0x0025ca
342 \<wrong> code: 0x002240 group: relation
343 \<struct> code: 0x0022c4
344 \<acute> code: 0x0000b4
345 \<index> code: 0x000131
346 \<dieresis> code: 0x0000a8
347 \<cedilla> code: 0x0000b8
348 \<hungarumlaut> code: 0x0002dd
349 \<some> code: 0x0003f5
350 \<newline> code: 0x0023ce
351 \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
352 \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
353 \<here> code: 0x002302 font: IsabelleText
354 \<^sub> code: 0x0021e9 group: control font: IsabelleText
355 \<^sup> code: 0x0021e7 group: control font: IsabelleText
356 \<^bold> code: 0x002759 group: control font: IsabelleText
357 \<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_(
358 \<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_)
359 \<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^(
360 \<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^)