# 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: -^

\<^bsub>                code: 0x0021d8  abbrev: =_(

\<^esub>                code: 0x0021d9  abbrev: =_)

\<^bsup>                code: 0x0021d7  abbrev: =^(

\<^esup>                code: 0x0021d6  abbrev: =^)

\<^bold>                code: 0x002759  abbrev: -.