1 # Default interpretation of some Isabelle symbols
6 \<three> code: 0x01d7ef
10 \<seven> code: 0x01d7f3
11 \<eight> code: 0x01d7f4
12 \<nine> code: 0x01d7f5
117 \<alpha> code: 0x0003b1
118 \<beta> code: 0x0003b2
119 \<gamma> code: 0x0003b3
120 \<delta> code: 0x0003b4
121 \<epsilon> code: 0x0003b5
122 \<zeta> code: 0x0003b6
123 \<eta> code: 0x0003b7
124 \<theta> code: 0x0003b8
125 \<iota> code: 0x0003b9
126 \<kappa> code: 0x0003ba
127 \<lambda> code: 0x0003bb abbrev: %
132 \<rho> code: 0x0003c1
133 \<sigma> code: 0x0003c3
134 \<tau> code: 0x0003c4
135 \<upsilon> code: 0x0003c5
136 \<phi> code: 0x0003c6
137 \<chi> code: 0x0003c7
138 \<psi> code: 0x0003c8
139 \<omega> code: 0x0003c9
140 \<Gamma> code: 0x000393
141 \<Delta> code: 0x000394
142 \<Theta> code: 0x000398
143 \<Lambda> code: 0x00039b
146 \<Sigma> code: 0x0003a3
147 \<Upsilon> code: 0x0003a5
148 \<Phi> code: 0x0003a6
149 \<Psi> code: 0x0003a8
150 \<Omega> code: 0x0003a9
151 \<bool> code: 0x01d539
152 \<complex> code: 0x002102
153 \<nat> code: 0x002115
154 \<rat> code: 0x00211a
155 \<real> code: 0x00211d
156 \<int> code: 0x002124
157 \<leftarrow> code: 0x002190
158 \<longleftarrow> code: 0x0027f5
159 \<rightarrow> code: 0x002192 abbrev: ->
160 \<longrightarrow> code: 0x0027f6 abbrev: -->
161 \<Leftarrow> code: 0x0021d0
162 \<Longleftarrow> code: 0x0027f8
163 \<Rightarrow> code: 0x0021d2 abbrev: =>
164 \<Longrightarrow> code: 0x0027f9 abbrev: ==>
165 \<leftrightarrow> code: 0x002194
166 \<longleftrightarrow> code: 0x0027f7 abbrev: <->
167 \<Leftrightarrow> code: 0x0021d4
168 \<Longleftrightarrow> code: 0x0027fa abbrev: <=>
169 \<mapsto> code: 0x0021a6 abbrev: |->
170 \<longmapsto> code: 0x0027fc abbrev: |-->
171 \<midarrow> code: 0x002500
172 \<Midarrow> code: 0x002550
173 \<hookleftarrow> code: 0x0021a9
174 \<hookrightarrow> code: 0x0021aa
175 \<leftharpoondown> code: 0x0021bd
176 \<rightharpoondown> code: 0x0021c1
177 \<leftharpoonup> code: 0x0021bc
178 \<rightharpoonup> code: 0x0021c0
179 \<rightleftharpoons> code: 0x0021cc
180 \<leadsto> code: 0x00219d abbrev: ~>
181 \<downharpoonleft> code: 0x0021c3
182 \<downharpoonright> code: 0x0021c2
183 \<upharpoonleft> code: 0x0021bf
184 #\<upharpoonright> code: 0x0021be
185 \<restriction> code: 0x0021be
186 \<Colon> code: 0x002237
189 \<down> code: 0x002193
190 \<Down> code: 0x0021d3
191 \<updown> code: 0x002195
192 \<Updown> code: 0x0021d5
193 \<langle> code: 0x0027e8 abbrev: <.
194 \<rangle> code: 0x0027e9 abbrev: .>
195 \<lceil> code: 0x002308
196 \<rceil> code: 0x002309
197 \<lfloor> code: 0x00230a
198 \<rfloor> code: 0x00230b
199 \<lparr> code: 0x002987 abbrev: (|
200 \<rparr> code: 0x002988 abbrev: |)
201 \<lbrakk> code: 0x0027e6 abbrev: [|
202 \<rbrakk> code: 0x0027e7 abbrev: |]
203 \<lbrace> code: 0x002983 abbrev: {.
204 \<rbrace> code: 0x002984 abbrev: .}
205 \<guillemotleft> code: 0x0000ab abbrev: <<
206 \<guillemotright> code: 0x0000bb abbrev: >>
207 \<bottom> code: 0x0022a5
208 \<top> code: 0x0022a4
209 \<and> code: 0x002227 abbrev: /\
210 \<And> code: 0x0022c0 abbrev: !!
211 \<or> code: 0x002228 abbrev: \/
212 \<Or> code: 0x0022c1 abbrev: ??
213 \<forall> code: 0x002200 abbrev: !
214 \<exists> code: 0x002203 abbrev: ?
215 \<nexists> code: 0x002204 abbrev: ~?
216 \<not> code: 0x0000ac abbrev: ~
217 \<box> code: 0x0025a1
218 \<diamond> code: 0x0025c7
219 \<turnstile> code: 0x0022a2 abbrev: |-
220 \<Turnstile> code: 0x0022a8 abbrev: |=
221 \<tturnstile> code: 0x0022a9 abbrev: ||-
222 \<TTurnstile> code: 0x0022ab abbrev: ||=
223 \<stileturn> code: 0x0022a3 abbrev: -|
224 \<surd> code: 0x00221a
225 \<le> code: 0x002264 abbrev: <=
226 \<ge> code: 0x002265 abbrev: >=
227 \<lless> code: 0x00226a
228 \<ggreater> code: 0x00226b
229 \<lesssim> code: 0x002272
230 \<greatersim> code: 0x002273
231 \<lessapprox> code: 0x002a85
232 \<greaterapprox> code: 0x002a86
233 \<in> code: 0x002208 abbrev: :
234 \<notin> code: 0x002209 abbrev: ~:
235 \<subset> code: 0x002282
236 \<supset> code: 0x002283
237 \<subseteq> code: 0x002286 abbrev: (=
238 \<supseteq> code: 0x002287 abbrev: =)
239 \<sqsubset> code: 0x00228f
240 \<sqsupset> code: 0x002290
241 \<sqsubseteq> code: 0x002291 abbrev: [=
242 \<sqsupseteq> code: 0x002292 abbrev: =]
243 \<inter> code: 0x002229 abbrev: Int
244 \<Inter> code: 0x0022c2 abbrev: Inter
245 \<union> code: 0x00222a abbrev: Un
246 \<Union> code: 0x0022c3 abbrev: Union
247 \<squnion> code: 0x002294
248 \<Squnion> code: 0x002a06
249 \<sqinter> code: 0x002293
250 \<Sqinter> code: 0x002a05
251 \<setminus> code: 0x002216
252 \<propto> code: 0x00221d
253 \<uplus> code: 0x00228e
254 \<Uplus> code: 0x002a04
255 \<noteq> code: 0x002260 abbrev: ~=
256 \<sim> code: 0x00223c
257 \<doteq> code: 0x002250
258 \<simeq> code: 0x002243
259 \<approx> code: 0x002248
260 \<asymp> code: 0x00224d
261 \<cong> code: 0x002245
262 \<smile> code: 0x002323
263 \<equiv> code: 0x002261 abbrev: ==
264 \<frown> code: 0x002322
265 \<Join> code: 0x0022c8
266 \<bowtie> code: 0x002a1d
267 \<prec> code: 0x00227a
268 \<succ> code: 0x00227b
269 \<preceq> code: 0x00227c
270 \<succeq> code: 0x00227d
271 \<parallel> code: 0x002225 abbrev: ||
272 \<bar> code: 0x0000a6
273 \<plusminus> code: 0x0000b1
274 \<minusplus> code: 0x002213
275 \<times> code: 0x0000d7
276 \<div> code: 0x0000f7
277 \<cdot> code: 0x0022c5
278 \<star> code: 0x0022c6
279 \<bullet> code: 0x002219
280 \<circ> code: 0x002218
281 \<dagger> code: 0x002020
282 \<ddagger> code: 0x002021
283 \<lhd> code: 0x0022b2
284 \<rhd> code: 0x0022b3
285 \<unlhd> code: 0x0022b4
286 \<unrhd> code: 0x0022b5
287 \<triangleleft> code: 0x0025c3
288 \<triangleright> code: 0x0025b9
289 \<triangle> code: 0x0025b3
290 \<triangleq> code: 0x00225c
291 \<oplus> code: 0x002295 abbrev: +o
292 \<Oplus> code: 0x002a01 abbrev: +O
293 \<otimes> code: 0x002297 abbrev: *o
294 \<Otimes> code: 0x002a02 abbrev: *O
295 \<odot> code: 0x002299 abbrev: .o
296 \<Odot> code: 0x002a00 abbrev: .O
297 \<ominus> code: 0x002296 abbrev: -o
298 \<oslash> code: 0x002298 abbrev: /o
299 \<dots> code: 0x002026 abbrev: ...
300 \<cdots> code: 0x0022ef
301 \<Sum> code: 0x002211 abbrev: SUM
302 \<Prod> code: 0x00220f abbrev: PROD
303 \<Coprod> code: 0x002210
304 \<infinity> code: 0x00221e
305 \<integral> code: 0x00222b
306 \<ointegral> code: 0x00222e
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
317 \<flat> code: 0x00266d
318 \<natural> code: 0x00266e
319 \<sharp> code: 0x00266f
320 \<angle> code: 0x002220
321 \<copyright> code: 0x0000a9
322 \<registered> code: 0x0000ae
323 \<hyphen> code: 0x0000ad
324 \<inverse> code: 0x0000af
325 \<onesuperior> code: 0x0000b9
326 \<onequarter> code: 0x0000bc
327 \<twosuperior> code: 0x0000b2
328 \<onehalf> code: 0x0000bd
329 \<threesuperior> code: 0x0000b3
330 \<threequarters> code: 0x0000be
331 \<ordfeminine> code: 0x0000aa
332 \<ordmasculine> code: 0x0000ba
333 \<section> code: 0x0000a7
334 \<paragraph> code: 0x0000b6
335 \<exclamdown> code: 0x0000a1
336 \<questiondown> code: 0x0000bf
337 \<euro> code: 0x0020ac
338 \<pounds> code: 0x0000a3
339 \<yen> code: 0x0000a5
340 \<cent> code: 0x0000a2
341 \<currency> code: 0x0000a4
342 \<degree> code: 0x0000b0
343 \<amalg> code: 0x002a3f
344 \<mho> code: 0x002127
345 \<lozenge> code: 0x0025ca
347 \<wrong> code: 0x002240
348 \<struct> code: 0x0022c4
349 \<acute> code: 0x0000b4
350 \<index> code: 0x000131
351 \<dieresis> code: 0x0000a8
352 \<cedilla> code: 0x0000b8
353 \<hungarumlaut> code: 0x0002dd
354 \<spacespace> code: 0x002423
355 \<some> code: 0x0003f5
356 \<^sub> code: 0x0021e9 abbrev: =_
357 \<^sup> code: 0x0021e7 abbrev: =^
358 \<^isub> code: 0x0021e3 abbrev: -_
359 \<^isup> code: 0x0021e1 abbrev: -^
360 \<^bsub> code: 0x0021d8 abbrev: =_(
361 \<^esub> code: 0x0021d9 abbrev: =_)
362 \<^bsup> code: 0x0021d7 abbrev: =^(
363 \<^esup> code: 0x0021d6 abbrev: =^)
364 \<^bold> code: 0x002759 abbrev: -.