# Default interpretation of some Isabelle symbols
\<zero> code: 0x01d7ec
\<one> code: 0x01d7ed
\<two> code: 0x01d7ee
\<three> code: 0x01d7ef
\<four> code: 0x01d7f0
\<five> code: 0x01d7f1
\<six> code: 0x01d7f2
\<seven> code: 0x01d7f3
\<eight> code: 0x01d7f4
\<nine> code: 0x01d7f5
\<A> code: 0x01d49c
\<B> code: 0x00212c
\<C> code: 0x01d49e
\<D> code: 0x01d49f
\<E> code: 0x002130
\<F> code: 0x002131
\<G> code: 0x01d4a2
\<H> code: 0x00210b
\<I> code: 0x002110
\<J> code: 0x01d4a5
\<K> code: 0x01d4a6
\<L> code: 0x002112
\<M> code: 0x002133
\<N> code: 0x01d4a9
\<O> code: 0x01d4aa
\<P> code: 0x01d4ab
\<Q> code: 0x01d4ac
\<R> code: 0x00211b
\<S> code: 0x01d4ae
\<T> code: 0x01d4af
\<U> code: 0x01d4b0
\<V> code: 0x01d4b1
\<W> code: 0x01d4b2
\<X> code: 0x01d4b3
\<Y> code: 0x01d4b4
\<Z> code: 0x01d4b5
\<a> code: 0x01d5ba
\<b> code: 0x01d5bb
\<c> code: 0x01d5bc
\<d> code: 0x01d5bd
\<e> code: 0x01d5be
\<f> code: 0x01d5bf
\<g> code: 0x01d5c0
\<h> code: 0x01d5c1
\<i> code: 0x01d5c2
\<j> code: 0x01d5c3
\<k> code: 0x01d5c4
\<l> code: 0x01d5c5
\<m> code: 0x01d5c6
\<n> code: 0x01d5c7
\<o> code: 0x01d5c8
\<p> code: 0x01d5c9
\<q> code: 0x01d5ca
\<r> code: 0x01d5cb
\<s> code: 0x01d5cc
\<t> code: 0x01d5cd
\<u> code: 0x01d5ce
\<v> code: 0x01d5cf
\<w> code: 0x01d5d0
\<x> code: 0x01d5d1
\<y> code: 0x01d5d2
\<z> code: 0x01d5d3
\<AA> code: 0x01d504
\<BB> code: 0x01d505
\<CC> code: 0x00212d
\<DD> code: 0x01d507
\<EE> code: 0x01d508
\<FF> code: 0x01d509
\<GG> code: 0x01d50a
\<HH> code: 0x00210c
#\<II> code: 0x01d50c
\<JJ> code: 0x01d50d
\<KK> code: 0x01d50e
\<LL> code: 0x01d50f
\<MM> code: 0x01d510
\<NN> code: 0x01d511
\<OO> code: 0x01d512
\<PP> code: 0x01d513
\<QQ> code: 0x01d514
#\<RR> code: 0x01d515
\<SS> code: 0x01d516
\<TT> code: 0x01d517
\<UU> code: 0x01d518
\<VV> code: 0x01d519
\<WW> code: 0x01d51a
\<XX> code: 0x01d51b
\<YY> code: 0x01d51c
\<ZZ> code: 0x002128
\<aa> code: 0x01d51e
\<bb> code: 0x01d51f
\<cc> code: 0x01d520
\<dd> code: 0x01d521
\<ee> code: 0x01d522
\<ff> code: 0x01d523
\<gg> code: 0x01d524
\<hh> code: 0x01d525
\<ii> code: 0x01d526
\<jj> code: 0x01d527
\<kk> code: 0x01d528
\<ll> code: 0x01d529
\<mm> code: 0x01d52a
\<nn> code: 0x01d52b
\<oo> code: 0x01d52c
\<pp> code: 0x01d52d
\<qq> code: 0x01d52e
\<rr> code: 0x01d52f
\<ss> code: 0x01d530
\<tt> code: 0x01d531
\<uu> code: 0x01d532
\<vv> code: 0x01d533
\<ww> code: 0x01d534
\<xx> code: 0x01d535
\<yy> code: 0x01d536
\<zz> code: 0x01d537
\<alpha> code: 0x0003b1
\<beta> code: 0x0003b2
\<gamma> code: 0x0003b3
\<delta> code: 0x0003b4
\<epsilon> code: 0x0003b5
\<zeta> code: 0x0003b6
\<eta> code: 0x0003b7
\<theta> code: 0x0003b8
\<iota> code: 0x0003b9
\<kappa> code: 0x0003ba
\<lambda> code: 0x0003bb abbrev: %
\<mu> code: 0x0003bc
\<nu> code: 0x0003bd
\<xi> code: 0x0003be
\<pi> code: 0x0003c0
\<rho> code: 0x0003c1
\<sigma> code: 0x0003c3
\<tau> code: 0x0003c4
\<upsilon> code: 0x0003c5
\<phi> code: 0x0003c6
\<chi> code: 0x0003c7
\<psi> code: 0x0003c8
\<omega> code: 0x0003c9
\<Gamma> code: 0x000393
\<Delta> code: 0x000394
\<Theta> code: 0x000398
\<Lambda> code: 0x00039b
\<Xi> code: 0x00039e
\<Pi> code: 0x0003a0
\<Sigma> code: 0x0003a3
\<Upsilon> code: 0x0003a5
\<Phi> code: 0x0003a6
\<Psi> code: 0x0003a8
\<Omega> code: 0x0003a9
\<bool> code: 0x01d539
\<complex> code: 0x002102
\<nat> code: 0x002115
\<rat> code: 0x00211a
\<real> code: 0x00211d
\<int> code: 0x002124
\<leftarrow> code: 0x002190
\<longleftarrow> code: 0x0027f5
\<rightarrow> code: 0x002192 abbrev: ->
\<longrightarrow> code: 0x0027f6 abbrev: -->
\<Leftarrow> code: 0x0021d0
\<Longleftarrow> code: 0x0027f8
\<Rightarrow> code: 0x0021d2 abbrev: =>
\<Longrightarrow> code: 0x0027f9 abbrev: ==>
\<leftrightarrow> code: 0x002194
\<longleftrightarrow> code: 0x0027f7 abbrev: <->
\<Leftrightarrow> code: 0x0021d4
\<Longleftrightarrow> code: 0x0027fa abbrev: <=>
\<mapsto> code: 0x0021a6 abbrev: |->
\<longmapsto> code: 0x0027fc abbrev: |-->
\<midarrow> code: 0x002500
\<Midarrow> code: 0x002550
\<hookleftarrow> code: 0x0021a9
\<hookrightarrow> code: 0x0021aa
\<leftharpoondown> code: 0x0021bd
\<rightharpoondown> code: 0x0021c1
\<leftharpoonup> code: 0x0021bc
\<rightharpoonup> code: 0x0021c0
\<rightleftharpoons> code: 0x0021cc
\<leadsto> code: 0x00219d abbrev: ~>
\<downharpoonleft> code: 0x0021c3
\<downharpoonright> code: 0x0021c2
\<upharpoonleft> code: 0x0021bf
#\<upharpoonright> code: 0x0021be
\<restriction> code: 0x0021be
\<Colon> code: 0x002237
\<up> code: 0x002191
\<Up> code: 0x0021d1
\<down> code: 0x002193
\<Down> code: 0x0021d3
\<updown> code: 0x002195
\<Updown> code: 0x0021d5
\<langle> code: 0x0027e8 abbrev: <.
\<rangle> code: 0x0027e9 abbrev: .>
\<lceil> code: 0x002308
\<rceil> code: 0x002309
\<lfloor> code: 0x00230a
\<rfloor> code: 0x00230b
\<lparr> code: 0x002987 abbrev: (|
\<rparr> code: 0x002988 abbrev: |)
\<lbrakk> code: 0x0027e6 abbrev: [|
\<rbrakk> code: 0x0027e7 abbrev: |]
\<lbrace> code: 0x002983 abbrev: {.
\<rbrace> code: 0x002984 abbrev: .}
\<guillemotleft> code: 0x0000ab abbrev: <<
\<guillemotright> code: 0x0000bb abbrev: >>
\<bottom> code: 0x0022a5
\<top> code: 0x0022a4
\<and> code: 0x002227 abbrev: /\
\<And> code: 0x0022c0 abbrev: !!
\<or> code: 0x002228 abbrev: \/
\<Or> code: 0x0022c1 abbrev: ??
\<forall> code: 0x002200 abbrev: !
\<exists> code: 0x002203 abbrev: ?
\<nexists> code: 0x002204 abbrev: ~?
\<not> code: 0x0000ac abbrev: ~
\<box> code: 0x0025a1
\<diamond> code: 0x0025c7
\<turnstile> code: 0x0022a2 abbrev: |-
\<Turnstile> code: 0x0022a8 abbrev: |=
\<tturnstile> code: 0x0022a9 abbrev: ||-
\<TTurnstile> code: 0x0022ab abbrev: ||=
\<stileturn> code: 0x0022a3 abbrev: -|
\<surd> code: 0x00221a
\<le> code: 0x002264 abbrev: <=
\<ge> code: 0x002265 abbrev: >=
\<lless> code: 0x00226a
\<ggreater> code: 0x00226b
\<lesssim> code: 0x002272
\<greatersim> code: 0x002273
\<lessapprox> code: 0x002a85
\<greaterapprox> code: 0x002a86
\<in> code: 0x002208 abbrev: :
\<notin> code: 0x002209 abbrev: ~:
\<subset> code: 0x002282
\<supset> code: 0x002283
\<subseteq> code: 0x002286 abbrev: (=
\<supseteq> code: 0x002287 abbrev: =)
\<sqsubset> code: 0x00228f
\<sqsupset> code: 0x002290
\<sqsubseteq> code: 0x002291 abbrev: [=
\<sqsupseteq> code: 0x002292 abbrev: =]
\<inter> code: 0x002229 abbrev: Int
\<Inter> code: 0x0022c2 abbrev: Inter
\<union> code: 0x00222a abbrev: Un
\<Union> code: 0x0022c3 abbrev: Union
\<squnion> code: 0x002294
\<Squnion> code: 0x002a06
\<sqinter> code: 0x002293
\<Sqinter> code: 0x002a05
\<setminus> code: 0x002216
\<propto> code: 0x00221d
\<uplus> code: 0x00228e
\<Uplus> code: 0x002a04
\<noteq> code: 0x002260 abbrev: ~=
\<sim> code: 0x00223c
\<doteq> code: 0x002250
\<simeq> code: 0x002243
\<approx> code: 0x002248
\<asymp> code: 0x00224d
\<cong> code: 0x002245
\<smile> code: 0x002323
\<equiv> code: 0x002261 abbrev: ==
\<frown> code: 0x002322
\<Join> code: 0x0022c8
\<bowtie> code: 0x002a1d
\<prec> code: 0x00227a
\<succ> code: 0x00227b
\<preceq> code: 0x00227c
\<succeq> code: 0x00227d
\<parallel> code: 0x002225 abbrev: ||
\<bar> code: 0x0000a6
\<plusminus> code: 0x0000b1
\<minusplus> code: 0x002213
\<times> code: 0x0000d7
\<div> code: 0x0000f7
\<cdot> code: 0x0022c5
\<star> code: 0x0022c6
\<bullet> code: 0x002219
\<circ> code: 0x002218
\<dagger> code: 0x002020
\<ddagger> code: 0x002021
\<lhd> code: 0x0022b2
\<rhd> code: 0x0022b3
\<unlhd> code: 0x0022b4
\<unrhd> code: 0x0022b5
\<triangleleft> code: 0x0025c3
\<triangleright> code: 0x0025b9
\<triangle> code: 0x0025b3
\<triangleq> code: 0x00225c
\<oplus> code: 0x002295 abbrev: +o
\<Oplus> code: 0x002a01 abbrev: +O
\<otimes> code: 0x002297 abbrev: *o
\<Otimes> code: 0x002a02 abbrev: *O
\<odot> code: 0x002299 abbrev: .o
\<Odot> code: 0x002a00 abbrev: .O
\<ominus> code: 0x002296 abbrev: -o
\<oslash> code: 0x002298 abbrev: /o
\<dots> code: 0x002026 abbrev: ...
\<cdots> code: 0x0022ef
\<Sum> code: 0x002211 abbrev: SUM
\<Prod> code: 0x00220f abbrev: PROD
\<Coprod> code: 0x002210
\<infinity> code: 0x00221e
\<integral> code: 0x00222b
\<ointegral> code: 0x00222e
\<clubsuit> code: 0x002663
\<diamondsuit> code: 0x002662
\<heartsuit> code: 0x002661
\<spadesuit> code: 0x002660
\<aleph> code: 0x002135
\<emptyset> code: 0x002205
\<nabla> code: 0x002207
\<partial> code: 0x002202
\<Re> code: 0x00211c
\<Im> code: 0x002111
\<flat> code: 0x00266d
\<natural> code: 0x00266e
\<sharp> code: 0x00266f
\<angle> code: 0x002220
\<copyright> code: 0x0000a9
\<registered> code: 0x0000ae
\<hyphen> code: 0x0000ad
\<inverse> code: 0x0000af
\<onesuperior> code: 0x0000b9
\<onequarter> code: 0x0000bc
\<twosuperior> code: 0x0000b2
\<onehalf> code: 0x0000bd
\<threesuperior> code: 0x0000b3
\<threequarters> code: 0x0000be
\<ordfeminine> code: 0x0000aa
\<ordmasculine> code: 0x0000ba
\<section> code: 0x0000a7
\<paragraph> code: 0x0000b6
\<exclamdown> code: 0x0000a1
\<questiondown> code: 0x0000bf
\<euro> code: 0x0020ac
\<pounds> code: 0x0000a3
\<yen> code: 0x0000a5
\<cent> code: 0x0000a2
\<currency> code: 0x0000a4
\<degree> code: 0x0000b0
\<amalg> code: 0x002a3f
\<mho> code: 0x002127
\<lozenge> code: 0x0025ca
\<wp> code: 0x002118
\<wrong> code: 0x002240
\<struct> code: 0x0022c4
\<acute> code: 0x0000b4
\<index> code: 0x000131
\<dieresis> code: 0x0000a8
\<cedilla> code: 0x0000b8
\<hungarumlaut> code: 0x0002dd
\<spacespace> code: 0x002423
\<some> code: 0x0003f5
\<^sub> code: 0x0021e9 abbrev: =_
\<^sup> code: 0x0021e7 abbrev: =^
\<^isub> code: 0x0021e3 abbrev: -_
\<^isup> code: 0x0021e1 abbrev: -^
\<^bold> code: 0x002759 abbrev: -.