# $Id$

# Default interpretation of some Isabelle symbols

symbol: \<zero>                 code: 0x01d7ec

symbol: \<one>                  code: 0x01d7ed

symbol: \<two>                  code: 0x01d7ee

symbol: \<three>                code: 0x01d7ef

symbol: \<four>                 code: 0x01d7f0

symbol: \<five>                 code: 0x01d7f1

symbol: \<six>                  code: 0x01d7f2

symbol: \<seven>                code: 0x01d7f3

symbol: \<eight>                code: 0x01d7f4

symbol: \<nine>                 code: 0x01d7f5

symbol: \<A>                    code: 0x01d49c

symbol: \<B>                    code: 0x00212c

symbol: \<C>                    code: 0x01d49e

symbol: \<D>                    code: 0x01d49f

symbol: \<E>                    code: 0x002130

symbol: \<F>                    code: 0x002131

symbol: \<G>                    code: 0x01d4a2

symbol: \<H>                    code: 0x00210b

symbol: \<I>                    code: 0x002110

symbol: \<J>                    code: 0x01d4a5

symbol: \<K>                    code: 0x01d4a6

symbol: \<L>                    code: 0x002112

symbol: \<M>                    code: 0x002133

symbol: \<N>                    code: 0x01d4a9

symbol: \<O>                    code: 0x01d4aa

symbol: \<P>                    code: 0x01d4ab

symbol: \<Q>                    code: 0x01d4ac

symbol: \<R>                    code: 0x00211b

symbol: \<S>                    code: 0x01d4ae

symbol: \<T>                    code: 0x01d4af

symbol: \<U>                    code: 0x01d4b0

symbol: \<V>                    code: 0x01d4b1

symbol: \<W>                    code: 0x01d4b2

symbol: \<X>                    code: 0x01d4b3

symbol: \<Y>                    code: 0x01d4b4

symbol: \<Z>                    code: 0x01d4b5

symbol: \<a>                    code: 0x01d5ba

symbol: \<b>                    code: 0x01d5bb

symbol: \<c>                    code: 0x01d5bc

symbol: \<d>                    code: 0x01d5bd

symbol: \<e>                    code: 0x01d5be

symbol: \<f>                    code: 0x01d5bf

symbol: \<g>                    code: 0x01d5c0

symbol: \<h>                    code: 0x01d5c1

symbol: \<i>                    code: 0x01d5c2

symbol: \<j>                    code: 0x01d5c3

symbol: \<k>                    code: 0x01d5c4

symbol: \<l>                    code: 0x01d5c5

symbol: \<m>                    code: 0x01d5c6

symbol: \<n>                    code: 0x01d5c7

symbol: \<o>                    code: 0x01d5c8

symbol: \<p>                    code: 0x01d5c9

symbol: \<q>                    code: 0x01d5ca

symbol: \<r>                    code: 0x01d5cb

symbol: \<s>                    code: 0x01d5cc

symbol: \<t>                    code: 0x01d5cd

symbol: \<u>                    code: 0x01d5ce

symbol: \<v>                    code: 0x01d5cf

symbol: \<w>                    code: 0x01d5d0

symbol: \<x>                    code: 0x01d5d1

symbol: \<y>                    code: 0x01d5d2

symbol: \<z>                    code: 0x01d5d3

symbol: \<AA>                   code: 0x01d504

symbol: \<BB>                   code: 0x01d505

symbol: \<CC>                   code: 0x00212d

symbol: \<DD>                   code: 0x01d507

symbol: \<EE>                   code: 0x01d508

symbol: \<FF>                   code: 0x01d509

symbol: \<GG>                   code: 0x01d50a

symbol: \<HH>                   code: 0x00210c

symbol: \<II>                   code: 0x002111

symbol: \<JJ>                   code: 0x01d50d

symbol: \<KK>                   code: 0x01d50e

symbol: \<LL>                   code: 0x01d50f

symbol: \<MM>                   code: 0x01d510

symbol: \<NN>                   code: 0x01d511

symbol: \<OO>                   code: 0x01d512

symbol: \<PP>                   code: 0x01d513

symbol: \<QQ>                   code: 0x01d514

symbol: \<RR>                   code: 0x00211c

symbol: \<SS>                   code: 0x01d516

symbol: \<TT>                   code: 0x01d517

symbol: \<UU>                   code: 0x01d518

symbol: \<VV>                   code: 0x01d519

symbol: \<WW>                   code: 0x01d51a

symbol: \<XX>                   code: 0x01d51b

symbol: \<YY>                   code: 0x01d51c

symbol: \<ZZ>                   code: 0x002128

symbol: \<aa>                   code: 0x01d51e

symbol: \<bb>                   code: 0x01d51f

symbol: \<cc>                   code: 0x01d520

symbol: \<dd>                   code: 0x01d521

symbol: \<ee>                   code: 0x01d522

symbol: \<ff>                   code: 0x01d523

symbol: \<gg>                   code: 0x01d524

symbol: \<hh>                   code: 0x01d525

symbol: \<ii>                   code: 0x01d526

symbol: \<jj>                   code: 0x01d527

symbol: \<kk>                   code: 0x01d528

symbol: \<ll>                   code: 0x01d529

symbol: \<mm>                   code: 0x01d52a

symbol: \<nn>                   code: 0x01d52b

symbol: \<oo>                   code: 0x01d52c

symbol: \<pp>                   code: 0x01d52d

symbol: \<qq>                   code: 0x01d52e

symbol: \<rr>                   code: 0x01d52f

symbol: \<ss>                   code: 0x01d530

symbol: \<tt>                   code: 0x01d531

symbol: \<uu>                   code: 0x01d532

symbol: \<vv>                   code: 0x01d533

symbol: \<ww>                   code: 0x01d534

symbol: \<xx>                   code: 0x01d535

symbol: \<yy>                   code: 0x01d536

symbol: \<zz>                   code: 0x01d537

symbol: \<alpha>                code: 0x0003b1

symbol: \<beta>                 code: 0x0003b2

symbol: \<gamma>                code: 0x0003b3

symbol: \<delta>                code: 0x0003b4

symbol: \<epsilon>              code: 0x0003b5

symbol: \<zeta>                 code: 0x0003b6

symbol: \<eta>                  code: 0x0003b7

symbol: \<theta>                code: 0x0003b8

symbol: \<iota>                 code: 0x0003b9

symbol: \<kappa>                code: 0x0003ba

symbol: \<lambda>               code: 0x0003bb

symbol: \<mu>                   code: 0x0003bc

symbol: \<nu>                   code: 0x0003bd

symbol: \<xi>                   code: 0x0003be

symbol: \<pi>                   code: 0x0003c0

symbol: \<rho>                  code: 0x0003c1

symbol: \<sigma>                code: 0x0003c3

symbol: \<tau>                  code: 0x0003c4

symbol: \<upsilon>              code: 0x0003c5

symbol: \<phi>                  code: 0x0003c6

symbol: \<chi>                  code: 0x0003c7

symbol: \<psi>                  code: 0x0003c8

symbol: \<omega>                code: 0x0003c9

symbol: \<Gamma>                code: 0x000393

symbol: \<Delta>                code: 0x000394

symbol: \<Theta>                code: 0x000398

symbol: \<Lambda>               code: 0x00039b

symbol: \<Xi>                   code: 0x00039e

symbol: \<Pi>                   code: 0x0003a0

symbol: \<Sigma>                code: 0x0003a3

symbol: \<Upsilon>              code: 0x0003a5

symbol: \<Phi>                  code: 0x0003a6

symbol: \<Psi>                  code: 0x0003a8

symbol: \<Omega>                code: 0x0003a9

symbol: \<bool>                 code: 0x01d539

symbol: \<complex>              code: 0x002102

symbol: \<nat>                  code: 0x002115

symbol: \<rat>                  code: 0x00211a

symbol: \<real>                 code: 0x00211d

symbol: \<int>                  code: 0x002124

symbol: \<leftarrow>            code: 0x002190

symbol: \<longleftarrow>        code: 0x0027f5

symbol: \<rightarrow>           code: 0x002192

symbol: \<longrightarrow>       code: 0x0027f6

symbol: \<Leftarrow>            code: 0x0021d0

symbol: \<Longleftarrow>        code: 0x0027f8

symbol: \<Rightarrow>           code: 0x0021d2

symbol: \<Longrightarrow>       code: 0x0027f9

symbol: \<leftrightarrow>       code: 0x002194

symbol: \<longleftrightarrow>   code: 0x0027f7

symbol: \<Leftrightarrow>       code: 0x0021d4

symbol: \<Longleftrightarrow>   code: 0x0027fa

symbol: \<mapsto>               code: 0x0021a6

symbol: \<longmapsto>           code: 0x0027fc

symbol: \<midarrow>             code: 0x002500

symbol: \<Midarrow>             code: 0x002550

symbol: \<hookleftarrow>        code: 0x0021a9

symbol: \<hookrightarrow>       code: 0x0021aa

symbol: \<leftharpoondown>      code: 0x0021bd

symbol: \<rightharpoondown>     code: 0x0021c1

symbol: \<leftharpoonup>        code: 0x0021bc

symbol: \<rightharpoonup>       code: 0x0021c0

symbol: \<rightleftharpoons>    code: 0x0021cc

symbol: \<leadsto>              code: 0x00219d

symbol: \<downharpoonleft>      code: 0x0021c3

symbol: \<downharpoonright>     code: 0x0021c2

symbol: \<upharpoonleft>        code: 0x0021bf

symbol: \<upharpoonright>       code: 0x0021be

symbol: \<restriction>          code: 0x0021be

symbol: \<Colon>                code: 0x002237

symbol: \<up>                   code: 0x002191

symbol: \<Up>                   code: 0x0021d1

symbol: \<down>                 code: 0x002193

symbol: \<Down>                 code: 0x0021d3

symbol: \<updown>               code: 0x002195

symbol: \<Updown>               code: 0x0021d5

symbol: \<langle>               code: 0x0027e8

symbol: \<rangle>               code: 0x0027e9

symbol: \<lceil>                code: 0x002308

symbol: \<rceil>                code: 0x002309

symbol: \<lfloor>               code: 0x00230a

symbol: \<rfloor>               code: 0x00230b

symbol: \<lparr>                code: 0x002987

symbol: \<rparr>                code: 0x002988

symbol: \<lbrakk>               code: 0x0027e6

symbol: \<rbrakk>               code: 0x0027e7

symbol: \<lbrace>               code: 0x002983

symbol: \<rbrace>               code: 0x002984

symbol: \<guillemotleft>        code: 0x0000ab

symbol: \<guillemotright>       code: 0x0000bb

symbol: \<bottom>               code: 0x0022a5

symbol: \<top>                  code: 0x0022a4

symbol: \<and>                  code: 0x002227

symbol: \<And>                  code: 0x0022c0

symbol: \<or>                   code: 0x002228

symbol: \<Or>                   code: 0x0022c1

symbol: \<forall>               code: 0x002200

symbol: \<exists>               code: 0x002203

symbol: \<nexists>              code: 0x002204

symbol: \<not>                  code: 0x0000ac

symbol: \<box>                  code: 0x0025a1

symbol: \<diamond>              code: 0x0025c7

symbol: \<turnstile>            code: 0x0022a2

symbol: \<Turnstile>            code: 0x0022a8

symbol: \<tturnstile>           code: 0x0022a9

symbol: \<TTurnstile>           code: 0x0022ab

symbol: \<stileturn>            code: 0x0022a3

symbol: \<surd>                 code: 0x00221a

symbol: \<le>                   code: 0x002264

symbol: \<ge>                   code: 0x002265

symbol: \<lless>                code: 0x00226a

symbol: \<ggreater>             code: 0x00226b

symbol: \<lesssim>              code: 0x002272

symbol: \<greatersim>           code: 0x002273

symbol: \<lessapprox>           code: 0x002a85

symbol: \<greaterapprox>        code: 0x002a86

symbol: \<in>                   code: 0x002208

symbol: \<notin>                code: 0x002209

symbol: \<subset>               code: 0x002282

symbol: \<supset>               code: 0x002283

symbol: \<subseteq>             code: 0x002286

symbol: \<supseteq>             code: 0x002287

symbol: \<sqsubset>             code: 0x00228f

symbol: \<sqsupset>             code: 0x002290

symbol: \<sqsubseteq>           code: 0x002291

symbol: \<sqsupseteq>           code: 0x002292

symbol: \<inter>                code: 0x002229

symbol: \<Inter>                code: 0x0022c2

symbol: \<union>                code: 0x00222a

symbol: \<Union>                code: 0x0022c3

symbol: \<squnion>              code: 0x002294

symbol: \<Squnion>              code: 0x002a06

symbol: \<sqinter>              code: 0x002293

symbol: \<Sqinter>              code: 0x002a05

symbol: \<setminus>             code: 0x002216

symbol: \<propto>               code: 0x00221d

symbol: \<uplus>                code: 0x00228e

symbol: \<Uplus>                code: 0x002a04

symbol: \<noteq>                code: 0x002260

symbol: \<sim>                  code: 0x00223c

symbol: \<doteq>                code: 0x002250

symbol: \<simeq>                code: 0x002243

symbol: \<approx>               code: 0x002248

symbol: \<asymp>                code: 0x00224d

symbol: \<cong>                 code: 0x002245

symbol: \<smile>                code: 0x002323

symbol: \<equiv>                code: 0x002261

symbol: \<frown>                code: 0x002322

symbol: \<Join>                 code: 0x0022c8

symbol: \<bowtie>               code: 0x002a1d

symbol: \<prec>                 code: 0x00227a

symbol: \<succ>                 code: 0x00227b

symbol: \<preceq>               code: 0x00227c

symbol: \<succeq>               code: 0x00227d

symbol: \<parallel>             code: 0x002225

symbol: \<bar>                  code: 0x0000a6

symbol: \<plusminus>            code: 0x0000b1

symbol: \<minusplus>            code: 0x002213

symbol: \<times>                code: 0x0000d7

symbol: \<div>                  code: 0x0000f7

symbol: \<cdot>                 code: 0x0022c5

symbol: \<star>                 code: 0x0022c6

symbol: \<bullet>               code: 0x002219

symbol: \<circ>                 code: 0x002218

symbol: \<dagger>               code: 0x002020

symbol: \<ddagger>              code: 0x002021

symbol: \<lhd>                  code: 0x0022b2

symbol: \<rhd>                  code: 0x0022b3

symbol: \<unlhd>                code: 0x0022b4

symbol: \<unrhd>                code: 0x0022b5

symbol: \<triangleleft>         code: 0x0025c3

symbol: \<triangleright>        code: 0x0025b9

symbol: \<triangle>             code: 0x0025b3

symbol: \<triangleq>            code: 0x00225c

symbol: \<oplus>                code: 0x002295

symbol: \<Oplus>                code: 0x002a01

symbol: \<otimes>               code: 0x002297

symbol: \<Otimes>               code: 0x002a02

symbol: \<odot>                 code: 0x002299

symbol: \<Odot>                 code: 0x002a00

symbol: \<ominus>               code: 0x002296

symbol: \<oslash>               code: 0x002298

symbol: \<dots>                 code: 0x002026

symbol: \<cdots>                code: 0x0022ef

symbol: \<Sum>                  code: 0x002211

symbol: \<Prod>                 code: 0x00220f

symbol: \<Coprod>               code: 0x002210

symbol: \<infinity>             code: 0x00221e

symbol: \<integral>             code: 0x00222b

symbol: \<ointegral>            code: 0x00222e

symbol: \<clubsuit>             code: 0x002663

symbol: \<diamondsuit>          code: 0x002662

symbol: \<heartsuit>            code: 0x002661

symbol: \<spadesuit>            code: 0x002660

symbol: \<aleph>                code: 0x002135

symbol: \<emptyset>             code: 0x002205

symbol: \<nabla>                code: 0x002207

symbol: \<partial>              code: 0x002202

symbol: \<Re>                   code: 0x00211c

symbol: \<Im>                   code: 0x002111

symbol: \<flat>                 code: 0x00266d

symbol: \<natural>              code: 0x00266e

symbol: \<sharp>                code: 0x00266f

symbol: \<angle>                code: 0x002220

symbol: \<copyright>            code: 0x0000a9

symbol: \<registered>           code: 0x0000ae

symbol: \<hyphen>               code: 0x0000ad

symbol: \<inverse>              code: 0x0000af

symbol: \<onesuperior>          code: 0x0000b9

symbol: \<onequarter>           code: 0x0000bc

symbol: \<twosuperior>          code: 0x0000b2

symbol: \<onehalf>              code: 0x0000bd

symbol: \<threesuperior>        code: 0x0000b3

symbol: \<threequarters>        code: 0x0000be

symbol: \<ordfeminine>          code: 0x0000aa

symbol: \<ordmasculine>         code: 0x0000ba

symbol: \<section>              code: 0x0000a7

symbol: \<paragraph>            code: 0x0000b6

symbol: \<exclamdown>           code: 0x0000a1

symbol: \<questiondown>         code: 0x0000bf

symbol: \<euro>                 code: 0x0020ac

symbol: \<pounds>               code: 0x0000a3

symbol: \<yen>                  code: 0x0000a5

symbol: \<cent>                 code: 0x0000a2

symbol: \<currency>             code: 0x0000a4

symbol: \<degree>               code: 0x0000b0

symbol: \<amalg>                code: 0x002a3f

symbol: \<mho>                  code: 0x002127

symbol: \<lozenge>              code: 0x0025ca

symbol: \<wp>                   code: 0x002118

symbol: \<wrong>                code: 0x002240

symbol: \<struct>               code: 0x0022c4

symbol: \<acute>                code: 0x0000b4

symbol: \<index>                code: 0x000131

symbol: \<dieresis>             code: 0x0000a8

symbol: \<cedilla>              code: 0x0000b8

symbol: \<hungarumlaut>         code: 0x0002dd

symbol: \<spacespace>           code: 0x002423

symbol: \<some>                 code: 0x0003f5