removed redundant "symbol" property;
authorwenzelm
Fri Aug 15 18:03:30 2008 +0200 (2008-08-15)
changeset 27899a152c8a38b7d
parent 27898 e0953043ce90
child 27900 fdd6e68e29d9
removed redundant "symbol" property;
added "font" propery;
disabled alternative letters (\<A> etc.) for now;
etc/symbols
     1.1 --- a/etc/symbols	Fri Aug 15 17:19:32 2008 +0200
     1.2 +++ b/etc/symbols	Fri Aug 15 18:03:30 2008 +0200
     1.3 @@ -1,357 +1,357 @@
     1.4  # $Id$
     1.5  # Default interpretation of some Isabelle symbols
     1.6  
     1.7 -symbol: \<zero>                 code: 0x01d7ec
     1.8 -symbol: \<one>                  code: 0x01d7ed
     1.9 -symbol: \<two>                  code: 0x01d7ee
    1.10 -symbol: \<three>                code: 0x01d7ef
    1.11 -symbol: \<four>                 code: 0x01d7f0
    1.12 -symbol: \<five>                 code: 0x01d7f1
    1.13 -symbol: \<six>                  code: 0x01d7f2
    1.14 -symbol: \<seven>                code: 0x01d7f3
    1.15 -symbol: \<eight>                code: 0x01d7f4
    1.16 -symbol: \<nine>                 code: 0x01d7f5
    1.17 -symbol: \<A>                    code: 0x01d49c
    1.18 -symbol: \<B>                    code: 0x00212c
    1.19 -symbol: \<C>                    code: 0x01d49e
    1.20 -symbol: \<D>                    code: 0x01d49f
    1.21 -symbol: \<E>                    code: 0x002130
    1.22 -symbol: \<F>                    code: 0x002131
    1.23 -symbol: \<G>                    code: 0x01d4a2
    1.24 -symbol: \<H>                    code: 0x00210b
    1.25 -symbol: \<I>                    code: 0x002110
    1.26 -symbol: \<J>                    code: 0x01d4a5
    1.27 -symbol: \<K>                    code: 0x01d4a6
    1.28 -symbol: \<L>                    code: 0x002112
    1.29 -symbol: \<M>                    code: 0x002133
    1.30 -symbol: \<N>                    code: 0x01d4a9
    1.31 -symbol: \<O>                    code: 0x01d4aa
    1.32 -symbol: \<P>                    code: 0x01d4ab
    1.33 -symbol: \<Q>                    code: 0x01d4ac
    1.34 -symbol: \<R>                    code: 0x00211b
    1.35 -symbol: \<S>                    code: 0x01d4ae
    1.36 -symbol: \<T>                    code: 0x01d4af
    1.37 -symbol: \<U>                    code: 0x01d4b0
    1.38 -symbol: \<V>                    code: 0x01d4b1
    1.39 -symbol: \<W>                    code: 0x01d4b2
    1.40 -symbol: \<X>                    code: 0x01d4b3
    1.41 -symbol: \<Y>                    code: 0x01d4b4
    1.42 -symbol: \<Z>                    code: 0x01d4b5
    1.43 -symbol: \<a>                    code: 0x01d5ba
    1.44 -symbol: \<b>                    code: 0x01d5bb
    1.45 -symbol: \<c>                    code: 0x01d5bc
    1.46 -symbol: \<d>                    code: 0x01d5bd
    1.47 -symbol: \<e>                    code: 0x01d5be
    1.48 -symbol: \<f>                    code: 0x01d5bf
    1.49 -symbol: \<g>                    code: 0x01d5c0
    1.50 -symbol: \<h>                    code: 0x01d5c1
    1.51 -symbol: \<i>                    code: 0x01d5c2
    1.52 -symbol: \<j>                    code: 0x01d5c3
    1.53 -symbol: \<k>                    code: 0x01d5c4
    1.54 -symbol: \<l>                    code: 0x01d5c5
    1.55 -symbol: \<m>                    code: 0x01d5c6
    1.56 -symbol: \<n>                    code: 0x01d5c7
    1.57 -symbol: \<o>                    code: 0x01d5c8
    1.58 -symbol: \<p>                    code: 0x01d5c9
    1.59 -symbol: \<q>                    code: 0x01d5ca
    1.60 -symbol: \<r>                    code: 0x01d5cb
    1.61 -symbol: \<s>                    code: 0x01d5cc
    1.62 -symbol: \<t>                    code: 0x01d5cd
    1.63 -symbol: \<u>                    code: 0x01d5ce
    1.64 -symbol: \<v>                    code: 0x01d5cf
    1.65 -symbol: \<w>                    code: 0x01d5d0
    1.66 -symbol: \<x>                    code: 0x01d5d1
    1.67 -symbol: \<y>                    code: 0x01d5d2
    1.68 -symbol: \<z>                    code: 0x01d5d3
    1.69 -symbol: \<AA>                   code: 0x01d504
    1.70 -symbol: \<BB>                   code: 0x01d505
    1.71 -symbol: \<CC>                   code: 0x00212d
    1.72 -symbol: \<DD>                   code: 0x01d507
    1.73 -symbol: \<EE>                   code: 0x01d508
    1.74 -symbol: \<FF>                   code: 0x01d509
    1.75 -symbol: \<GG>                   code: 0x01d50a
    1.76 -symbol: \<HH>                   code: 0x00210c
    1.77 -symbol: \<II>                   code: 0x002111
    1.78 -symbol: \<JJ>                   code: 0x01d50d
    1.79 -symbol: \<KK>                   code: 0x01d50e
    1.80 -symbol: \<LL>                   code: 0x01d50f
    1.81 -symbol: \<MM>                   code: 0x01d510
    1.82 -symbol: \<NN>                   code: 0x01d511
    1.83 -symbol: \<OO>                   code: 0x01d512
    1.84 -symbol: \<PP>                   code: 0x01d513
    1.85 -symbol: \<QQ>                   code: 0x01d514
    1.86 -symbol: \<RR>                   code: 0x00211c
    1.87 -symbol: \<SS>                   code: 0x01d516
    1.88 -symbol: \<TT>                   code: 0x01d517
    1.89 -symbol: \<UU>                   code: 0x01d518
    1.90 -symbol: \<VV>                   code: 0x01d519
    1.91 -symbol: \<WW>                   code: 0x01d51a
    1.92 -symbol: \<XX>                   code: 0x01d51b
    1.93 -symbol: \<YY>                   code: 0x01d51c
    1.94 -symbol: \<ZZ>                   code: 0x002128
    1.95 -symbol: \<aa>                   code: 0x01d51e
    1.96 -symbol: \<bb>                   code: 0x01d51f
    1.97 -symbol: \<cc>                   code: 0x01d520
    1.98 -symbol: \<dd>                   code: 0x01d521
    1.99 -symbol: \<ee>                   code: 0x01d522
   1.100 -symbol: \<ff>                   code: 0x01d523
   1.101 -symbol: \<gg>                   code: 0x01d524
   1.102 -symbol: \<hh>                   code: 0x01d525
   1.103 -symbol: \<ii>                   code: 0x01d526
   1.104 -symbol: \<jj>                   code: 0x01d527
   1.105 -symbol: \<kk>                   code: 0x01d528
   1.106 -symbol: \<ll>                   code: 0x01d529
   1.107 -symbol: \<mm>                   code: 0x01d52a
   1.108 -symbol: \<nn>                   code: 0x01d52b
   1.109 -symbol: \<oo>                   code: 0x01d52c
   1.110 -symbol: \<pp>                   code: 0x01d52d
   1.111 -symbol: \<qq>                   code: 0x01d52e
   1.112 -symbol: \<rr>                   code: 0x01d52f
   1.113 -symbol: \<ss>                   code: 0x01d530
   1.114 -symbol: \<tt>                   code: 0x01d531
   1.115 -symbol: \<uu>                   code: 0x01d532
   1.116 -symbol: \<vv>                   code: 0x01d533
   1.117 -symbol: \<ww>                   code: 0x01d534
   1.118 -symbol: \<xx>                   code: 0x01d535
   1.119 -symbol: \<yy>                   code: 0x01d536
   1.120 -symbol: \<zz>                   code: 0x01d537
   1.121 -symbol: \<alpha>                code: 0x0003b1
   1.122 -symbol: \<beta>                 code: 0x0003b2
   1.123 -symbol: \<gamma>                code: 0x0003b3
   1.124 -symbol: \<delta>                code: 0x0003b4
   1.125 -symbol: \<epsilon>              code: 0x0003b5
   1.126 -symbol: \<zeta>                 code: 0x0003b6
   1.127 -symbol: \<eta>                  code: 0x0003b7
   1.128 -symbol: \<theta>                code: 0x0003b8
   1.129 -symbol: \<iota>                 code: 0x0003b9
   1.130 -symbol: \<kappa>                code: 0x0003ba
   1.131 -symbol: \<lambda>               code: 0x0003bb
   1.132 -symbol: \<mu>                   code: 0x0003bc
   1.133 -symbol: \<nu>                   code: 0x0003bd
   1.134 -symbol: \<xi>                   code: 0x0003be
   1.135 -symbol: \<pi>                   code: 0x0003c0
   1.136 -symbol: \<rho>                  code: 0x0003c1
   1.137 -symbol: \<sigma>                code: 0x0003c3
   1.138 -symbol: \<tau>                  code: 0x0003c4
   1.139 -symbol: \<upsilon>              code: 0x0003c5
   1.140 -symbol: \<phi>                  code: 0x0003c6
   1.141 -symbol: \<chi>                  code: 0x0003c7
   1.142 -symbol: \<psi>                  code: 0x0003c8
   1.143 -symbol: \<omega>                code: 0x0003c9
   1.144 -symbol: \<Gamma>                code: 0x000393
   1.145 -symbol: \<Delta>                code: 0x000394
   1.146 -symbol: \<Theta>                code: 0x000398
   1.147 -symbol: \<Lambda>               code: 0x00039b
   1.148 -symbol: \<Xi>                   code: 0x00039e
   1.149 -symbol: \<Pi>                   code: 0x0003a0
   1.150 -symbol: \<Sigma>                code: 0x0003a3
   1.151 -symbol: \<Upsilon>              code: 0x0003a5
   1.152 -symbol: \<Phi>                  code: 0x0003a6
   1.153 -symbol: \<Psi>                  code: 0x0003a8
   1.154 -symbol: \<Omega>                code: 0x0003a9
   1.155 -symbol: \<bool>                 code: 0x01d539
   1.156 -symbol: \<complex>              code: 0x002102
   1.157 -symbol: \<nat>                  code: 0x002115
   1.158 -symbol: \<rat>                  code: 0x00211a
   1.159 -symbol: \<real>                 code: 0x00211d
   1.160 -symbol: \<int>                  code: 0x002124
   1.161 -symbol: \<leftarrow>            code: 0x002190
   1.162 -symbol: \<longleftarrow>        code: 0x0027f5
   1.163 -symbol: \<rightarrow>           code: 0x002192
   1.164 -symbol: \<longrightarrow>       code: 0x0027f6
   1.165 -symbol: \<Leftarrow>            code: 0x0021d0
   1.166 -symbol: \<Longleftarrow>        code: 0x0027f8
   1.167 -symbol: \<Rightarrow>           code: 0x0021d2
   1.168 -symbol: \<Longrightarrow>       code: 0x0027f9
   1.169 -symbol: \<leftrightarrow>       code: 0x002194
   1.170 -symbol: \<longleftrightarrow>   code: 0x0027f7
   1.171 -symbol: \<Leftrightarrow>       code: 0x0021d4
   1.172 -symbol: \<Longleftrightarrow>   code: 0x0027fa
   1.173 -symbol: \<mapsto>               code: 0x0021a6
   1.174 -symbol: \<longmapsto>           code: 0x0027fc
   1.175 -symbol: \<midarrow>             code: 0x002500
   1.176 -symbol: \<Midarrow>             code: 0x002550
   1.177 -symbol: \<hookleftarrow>        code: 0x0021a9
   1.178 -symbol: \<hookrightarrow>       code: 0x0021aa
   1.179 -symbol: \<leftharpoondown>      code: 0x0021bd
   1.180 -symbol: \<rightharpoondown>     code: 0x0021c1
   1.181 -symbol: \<leftharpoonup>        code: 0x0021bc
   1.182 -symbol: \<rightharpoonup>       code: 0x0021c0
   1.183 -symbol: \<rightleftharpoons>    code: 0x0021cc
   1.184 -symbol: \<leadsto>              code: 0x00219d
   1.185 -symbol: \<downharpoonleft>      code: 0x0021c3
   1.186 -symbol: \<downharpoonright>     code: 0x0021c2
   1.187 -symbol: \<upharpoonleft>        code: 0x0021bf
   1.188 -symbol: \<upharpoonright>       code: 0x0021be
   1.189 -symbol: \<restriction>          code: 0x0021be
   1.190 -symbol: \<Colon>                code: 0x002237
   1.191 -symbol: \<up>                   code: 0x002191
   1.192 -symbol: \<Up>                   code: 0x0021d1
   1.193 -symbol: \<down>                 code: 0x002193
   1.194 -symbol: \<Down>                 code: 0x0021d3
   1.195 -symbol: \<updown>               code: 0x002195
   1.196 -symbol: \<Updown>               code: 0x0021d5
   1.197 -symbol: \<langle>               code: 0x0027e8
   1.198 -symbol: \<rangle>               code: 0x0027e9
   1.199 -symbol: \<lceil>                code: 0x002308
   1.200 -symbol: \<rceil>                code: 0x002309
   1.201 -symbol: \<lfloor>               code: 0x00230a
   1.202 -symbol: \<rfloor>               code: 0x00230b
   1.203 -symbol: \<lparr>                code: 0x002987
   1.204 -symbol: \<rparr>                code: 0x002988
   1.205 -symbol: \<lbrakk>               code: 0x0027e6
   1.206 -symbol: \<rbrakk>               code: 0x0027e7
   1.207 -symbol: \<lbrace>               code: 0x002983
   1.208 -symbol: \<rbrace>               code: 0x002984
   1.209 -symbol: \<guillemotleft>        code: 0x0000ab
   1.210 -symbol: \<guillemotright>       code: 0x0000bb
   1.211 -symbol: \<bottom>               code: 0x0022a5
   1.212 -symbol: \<top>                  code: 0x0022a4
   1.213 -symbol: \<and>                  code: 0x002227
   1.214 -symbol: \<And>                  code: 0x0022c0
   1.215 -symbol: \<or>                   code: 0x002228
   1.216 -symbol: \<Or>                   code: 0x0022c1
   1.217 -symbol: \<forall>               code: 0x002200
   1.218 -symbol: \<exists>               code: 0x002203
   1.219 -symbol: \<nexists>              code: 0x002204
   1.220 -symbol: \<not>                  code: 0x0000ac
   1.221 -symbol: \<box>                  code: 0x0025a1
   1.222 -symbol: \<diamond>              code: 0x0025c7
   1.223 -symbol: \<turnstile>            code: 0x0022a2
   1.224 -symbol: \<Turnstile>            code: 0x0022a8
   1.225 -symbol: \<tturnstile>           code: 0x0022a9
   1.226 -symbol: \<TTurnstile>           code: 0x0022ab
   1.227 -symbol: \<stileturn>            code: 0x0022a3
   1.228 -symbol: \<surd>                 code: 0x00221a
   1.229 -symbol: \<le>                   code: 0x002264
   1.230 -symbol: \<ge>                   code: 0x002265
   1.231 -symbol: \<lless>                code: 0x00226a
   1.232 -symbol: \<ggreater>             code: 0x00226b
   1.233 -symbol: \<lesssim>              code: 0x002272
   1.234 -symbol: \<greatersim>           code: 0x002273
   1.235 -symbol: \<lessapprox>           code: 0x002a85
   1.236 -symbol: \<greaterapprox>        code: 0x002a86
   1.237 -symbol: \<in>                   code: 0x002208
   1.238 -symbol: \<notin>                code: 0x002209
   1.239 -symbol: \<subset>               code: 0x002282
   1.240 -symbol: \<supset>               code: 0x002283
   1.241 -symbol: \<subseteq>             code: 0x002286
   1.242 -symbol: \<supseteq>             code: 0x002287
   1.243 -symbol: \<sqsubset>             code: 0x00228f
   1.244 -symbol: \<sqsupset>             code: 0x002290
   1.245 -symbol: \<sqsubseteq>           code: 0x002291
   1.246 -symbol: \<sqsupseteq>           code: 0x002292
   1.247 -symbol: \<inter>                code: 0x002229
   1.248 -symbol: \<Inter>                code: 0x0022c2
   1.249 -symbol: \<union>                code: 0x00222a
   1.250 -symbol: \<Union>                code: 0x0022c3
   1.251 -symbol: \<squnion>              code: 0x002294
   1.252 -symbol: \<Squnion>              code: 0x002a06
   1.253 -symbol: \<sqinter>              code: 0x002293
   1.254 -symbol: \<Sqinter>              code: 0x002a05
   1.255 -symbol: \<setminus>             code: 0x002216
   1.256 -symbol: \<propto>               code: 0x00221d
   1.257 -symbol: \<uplus>                code: 0x00228e
   1.258 -symbol: \<Uplus>                code: 0x002a04
   1.259 -symbol: \<noteq>                code: 0x002260
   1.260 -symbol: \<sim>                  code: 0x00223c
   1.261 -symbol: \<doteq>                code: 0x002250
   1.262 -symbol: \<simeq>                code: 0x002243
   1.263 -symbol: \<approx>               code: 0x002248
   1.264 -symbol: \<asymp>                code: 0x00224d
   1.265 -symbol: \<cong>                 code: 0x002245
   1.266 -symbol: \<smile>                code: 0x002323
   1.267 -symbol: \<equiv>                code: 0x002261
   1.268 -symbol: \<frown>                code: 0x002322
   1.269 -symbol: \<Join>                 code: 0x0022c8
   1.270 -symbol: \<bowtie>               code: 0x002a1d
   1.271 -symbol: \<prec>                 code: 0x00227a
   1.272 -symbol: \<succ>                 code: 0x00227b
   1.273 -symbol: \<preceq>               code: 0x00227c
   1.274 -symbol: \<succeq>               code: 0x00227d
   1.275 -symbol: \<parallel>             code: 0x002225
   1.276 -symbol: \<bar>                  code: 0x0000a6
   1.277 -symbol: \<plusminus>            code: 0x0000b1
   1.278 -symbol: \<minusplus>            code: 0x002213
   1.279 -symbol: \<times>                code: 0x0000d7
   1.280 -symbol: \<div>                  code: 0x0000f7
   1.281 -symbol: \<cdot>                 code: 0x0022c5
   1.282 -symbol: \<star>                 code: 0x0022c6
   1.283 -symbol: \<bullet>               code: 0x002219
   1.284 -symbol: \<circ>                 code: 0x002218
   1.285 -symbol: \<dagger>               code: 0x002020
   1.286 -symbol: \<ddagger>              code: 0x002021
   1.287 -symbol: \<lhd>                  code: 0x0022b2
   1.288 -symbol: \<rhd>                  code: 0x0022b3
   1.289 -symbol: \<unlhd>                code: 0x0022b4
   1.290 -symbol: \<unrhd>                code: 0x0022b5
   1.291 -symbol: \<triangleleft>         code: 0x0025c3
   1.292 -symbol: \<triangleright>        code: 0x0025b9
   1.293 -symbol: \<triangle>             code: 0x0025b3
   1.294 -symbol: \<triangleq>            code: 0x00225c
   1.295 -symbol: \<oplus>                code: 0x002295
   1.296 -symbol: \<Oplus>                code: 0x002a01
   1.297 -symbol: \<otimes>               code: 0x002297
   1.298 -symbol: \<Otimes>               code: 0x002a02
   1.299 -symbol: \<odot>                 code: 0x002299
   1.300 -symbol: \<Odot>                 code: 0x002a00
   1.301 -symbol: \<ominus>               code: 0x002296
   1.302 -symbol: \<oslash>               code: 0x002298
   1.303 -symbol: \<dots>                 code: 0x002026
   1.304 -symbol: \<cdots>                code: 0x0022ef
   1.305 -symbol: \<Sum>                  code: 0x002211
   1.306 -symbol: \<Prod>                 code: 0x00220f
   1.307 -symbol: \<Coprod>               code: 0x002210
   1.308 -symbol: \<infinity>             code: 0x00221e
   1.309 -symbol: \<integral>             code: 0x00222b
   1.310 -symbol: \<ointegral>            code: 0x00222e
   1.311 -symbol: \<clubsuit>             code: 0x002663
   1.312 -symbol: \<diamondsuit>          code: 0x002662
   1.313 -symbol: \<heartsuit>            code: 0x002661
   1.314 -symbol: \<spadesuit>            code: 0x002660
   1.315 -symbol: \<aleph>                code: 0x002135
   1.316 -symbol: \<emptyset>             code: 0x002205
   1.317 -symbol: \<nabla>                code: 0x002207
   1.318 -symbol: \<partial>              code: 0x002202
   1.319 -symbol: \<Re>                   code: 0x00211c
   1.320 -symbol: \<Im>                   code: 0x002111
   1.321 -symbol: \<flat>                 code: 0x00266d
   1.322 -symbol: \<natural>              code: 0x00266e
   1.323 -symbol: \<sharp>                code: 0x00266f
   1.324 -symbol: \<angle>                code: 0x002220
   1.325 -symbol: \<copyright>            code: 0x0000a9
   1.326 -symbol: \<registered>           code: 0x0000ae
   1.327 -symbol: \<hyphen>               code: 0x0000ad
   1.328 -symbol: \<inverse>              code: 0x0000af
   1.329 -symbol: \<onesuperior>          code: 0x0000b9
   1.330 -symbol: \<onequarter>           code: 0x0000bc
   1.331 -symbol: \<twosuperior>          code: 0x0000b2
   1.332 -symbol: \<onehalf>              code: 0x0000bd
   1.333 -symbol: \<threesuperior>        code: 0x0000b3
   1.334 -symbol: \<threequarters>        code: 0x0000be
   1.335 -symbol: \<ordfeminine>          code: 0x0000aa
   1.336 -symbol: \<ordmasculine>         code: 0x0000ba
   1.337 -symbol: \<section>              code: 0x0000a7
   1.338 -symbol: \<paragraph>            code: 0x0000b6
   1.339 -symbol: \<exclamdown>           code: 0x0000a1
   1.340 -symbol: \<questiondown>         code: 0x0000bf
   1.341 -symbol: \<euro>                 code: 0x0020ac
   1.342 -symbol: \<pounds>               code: 0x0000a3
   1.343 -symbol: \<yen>                  code: 0x0000a5
   1.344 -symbol: \<cent>                 code: 0x0000a2
   1.345 -symbol: \<currency>             code: 0x0000a4
   1.346 -symbol: \<degree>               code: 0x0000b0
   1.347 -symbol: \<amalg>                code: 0x002a3f
   1.348 -symbol: \<mho>                  code: 0x002127
   1.349 -symbol: \<lozenge>              code: 0x0025ca
   1.350 -symbol: \<wp>                   code: 0x002118
   1.351 -symbol: \<wrong>                code: 0x002240
   1.352 -symbol: \<struct>               code: 0x0022c4
   1.353 -symbol: \<acute>                code: 0x0000b4
   1.354 -symbol: \<index>                code: 0x000131
   1.355 -symbol: \<dieresis>             code: 0x0000a8
   1.356 -symbol: \<cedilla>              code: 0x0000b8
   1.357 -symbol: \<hungarumlaut>         code: 0x0002dd
   1.358 -symbol: \<spacespace>           code: 0x002423
   1.359 -symbol: \<some>                 code: 0x0003f5
   1.360 +\<zero>                 code: 0x01d7ec  font: Isabelle
   1.361 +\<one>                  code: 0x01d7ed  font: Isabelle
   1.362 +\<two>                  code: 0x01d7ee  font: Isabelle
   1.363 +\<three>                code: 0x01d7ef  font: Isabelle
   1.364 +\<four>                 code: 0x01d7f0  font: Isabelle
   1.365 +\<five>                 code: 0x01d7f1  font: Isabelle
   1.366 +\<six>                  code: 0x01d7f2  font: Isabelle
   1.367 +\<seven>                code: 0x01d7f3  font: Isabelle
   1.368 +\<eight>                code: 0x01d7f4  font: Isabelle
   1.369 +\<nine>                 code: 0x01d7f5  font: Isabelle
   1.370 +#\<A>                    code: 0x01d49c
   1.371 +#\<B>                    code: 0x00212c
   1.372 +#\<C>                    code: 0x01d49e
   1.373 +#\<D>                    code: 0x01d49f
   1.374 +#\<E>                    code: 0x002130
   1.375 +#\<F>                    code: 0x002131
   1.376 +#\<G>                    code: 0x01d4a2
   1.377 +#\<H>                    code: 0x00210b
   1.378 +#\<I>                    code: 0x002110
   1.379 +#\<J>                    code: 0x01d4a5
   1.380 +#\<K>                    code: 0x01d4a6
   1.381 +#\<L>                    code: 0x002112
   1.382 +#\<M>                    code: 0x002133
   1.383 +#\<N>                    code: 0x01d4a9
   1.384 +#\<O>                    code: 0x01d4aa
   1.385 +#\<P>                    code: 0x01d4ab
   1.386 +#\<Q>                    code: 0x01d4ac
   1.387 +#\<R>                    code: 0x00211b
   1.388 +#\<S>                    code: 0x01d4ae
   1.389 +#\<T>                    code: 0x01d4af
   1.390 +#\<U>                    code: 0x01d4b0
   1.391 +#\<V>                    code: 0x01d4b1
   1.392 +#\<W>                    code: 0x01d4b2
   1.393 +#\<X>                    code: 0x01d4b3
   1.394 +#\<Y>                    code: 0x01d4b4
   1.395 +#\<Z>                    code: 0x01d4b5
   1.396 +#\<a>                    code: 0x01d5ba
   1.397 +#\<b>                    code: 0x01d5bb
   1.398 +#\<c>                    code: 0x01d5bc
   1.399 +#\<d>                    code: 0x01d5bd
   1.400 +#\<e>                    code: 0x01d5be
   1.401 +#\<f>                    code: 0x01d5bf
   1.402 +#\<g>                    code: 0x01d5c0
   1.403 +#\<h>                    code: 0x01d5c1
   1.404 +#\<i>                    code: 0x01d5c2
   1.405 +#\<j>                    code: 0x01d5c3
   1.406 +#\<k>                    code: 0x01d5c4
   1.407 +#\<l>                    code: 0x01d5c5
   1.408 +#\<m>                    code: 0x01d5c6
   1.409 +#\<n>                    code: 0x01d5c7
   1.410 +#\<o>                    code: 0x01d5c8
   1.411 +#\<p>                    code: 0x01d5c9
   1.412 +#\<q>                    code: 0x01d5ca
   1.413 +#\<r>                    code: 0x01d5cb
   1.414 +#\<s>                    code: 0x01d5cc
   1.415 +#\<t>                    code: 0x01d5cd
   1.416 +#\<u>                    code: 0x01d5ce
   1.417 +#\<v>                    code: 0x01d5cf
   1.418 +#\<w>                    code: 0x01d5d0
   1.419 +#\<x>                    code: 0x01d5d1
   1.420 +#\<y>                    code: 0x01d5d2
   1.421 +#\<z>                    code: 0x01d5d3
   1.422 +#\<AA>                   code: 0x01d504
   1.423 +#\<BB>                   code: 0x01d505
   1.424 +#\<CC>                   code: 0x00212d
   1.425 +#\<DD>                   code: 0x01d507
   1.426 +#\<EE>                   code: 0x01d508
   1.427 +#\<FF>                   code: 0x01d509
   1.428 +#\<GG>                   code: 0x01d50a
   1.429 +#\<HH>                   code: 0x00210c
   1.430 +#\<II>                   code: 0x002111
   1.431 +#\<JJ>                   code: 0x01d50d
   1.432 +#\<KK>                   code: 0x01d50e
   1.433 +#\<LL>                   code: 0x01d50f
   1.434 +#\<MM>                   code: 0x01d510
   1.435 +#\<NN>                   code: 0x01d511
   1.436 +#\<OO>                   code: 0x01d512
   1.437 +#\<PP>                   code: 0x01d513
   1.438 +#\<QQ>                   code: 0x01d514
   1.439 +#\<RR>                   code: 0x00211c
   1.440 +#\<SS>                   code: 0x01d516
   1.441 +#\<TT>                   code: 0x01d517
   1.442 +#\<UU>                   code: 0x01d518
   1.443 +#\<VV>                   code: 0x01d519
   1.444 +#\<WW>                   code: 0x01d51a
   1.445 +#\<XX>                   code: 0x01d51b
   1.446 +#\<YY>                   code: 0x01d51c
   1.447 +#\<ZZ>                   code: 0x002128
   1.448 +#\<aa>                   code: 0x01d51e
   1.449 +#\<bb>                   code: 0x01d51f
   1.450 +#\<cc>                   code: 0x01d520
   1.451 +#\<dd>                   code: 0x01d521
   1.452 +#\<ee>                   code: 0x01d522
   1.453 +#\<ff>                   code: 0x01d523
   1.454 +#\<gg>                   code: 0x01d524
   1.455 +#\<hh>                   code: 0x01d525
   1.456 +#\<ii>                   code: 0x01d526
   1.457 +#\<jj>                   code: 0x01d527
   1.458 +#\<kk>                   code: 0x01d528
   1.459 +#\<ll>                   code: 0x01d529
   1.460 +#\<mm>                   code: 0x01d52a
   1.461 +#\<nn>                   code: 0x01d52b
   1.462 +#\<oo>                   code: 0x01d52c
   1.463 +#\<pp>                   code: 0x01d52d
   1.464 +#\<qq>                   code: 0x01d52e
   1.465 +#\<rr>                   code: 0x01d52f
   1.466 +#\<ss>                   code: 0x01d530
   1.467 +#\<tt>                   code: 0x01d531
   1.468 +#\<uu>                   code: 0x01d532
   1.469 +#\<vv>                   code: 0x01d533
   1.470 +#\<ww>                   code: 0x01d534
   1.471 +#\<xx>                   code: 0x01d535
   1.472 +#\<yy>                   code: 0x01d536
   1.473 +#\<zz>                   code: 0x01d537
   1.474 +\<alpha>                code: 0x0003b1  font: Isabelle
   1.475 +\<beta>                 code: 0x0003b2  font: Isabelle
   1.476 +\<gamma>                code: 0x0003b3  font: Isabelle
   1.477 +\<delta>                code: 0x0003b4  font: Isabelle
   1.478 +\<epsilon>              code: 0x0003b5  font: Isabelle
   1.479 +\<zeta>                 code: 0x0003b6  font: Isabelle
   1.480 +\<eta>                  code: 0x0003b7  font: Isabelle
   1.481 +\<theta>                code: 0x0003b8  font: Isabelle
   1.482 +\<iota>                 code: 0x0003b9  font: Isabelle
   1.483 +\<kappa>                code: 0x0003ba  font: Isabelle
   1.484 +\<lambda>               code: 0x0003bb  font: Isabelle
   1.485 +\<mu>                   code: 0x0003bc  font: Isabelle
   1.486 +\<nu>                   code: 0x0003bd  font: Isabelle
   1.487 +\<xi>                   code: 0x0003be  font: Isabelle
   1.488 +\<pi>                   code: 0x0003c0  font: Isabelle
   1.489 +\<rho>                  code: 0x0003c1  font: Isabelle
   1.490 +\<sigma>                code: 0x0003c3  font: Isabelle
   1.491 +\<tau>                  code: 0x0003c4  font: Isabelle
   1.492 +\<upsilon>              code: 0x0003c5  font: Isabelle
   1.493 +\<phi>                  code: 0x0003c6  font: Isabelle
   1.494 +\<chi>                  code: 0x0003c7  font: Isabelle
   1.495 +\<psi>                  code: 0x0003c8  font: Isabelle
   1.496 +\<omega>                code: 0x0003c9  font: Isabelle
   1.497 +\<Gamma>                code: 0x000393  font: Isabelle
   1.498 +\<Delta>                code: 0x000394  font: Isabelle
   1.499 +\<Theta>                code: 0x000398  font: Isabelle
   1.500 +\<Lambda>               code: 0x00039b  font: Isabelle
   1.501 +\<Xi>                   code: 0x00039e  font: Isabelle
   1.502 +\<Pi>                   code: 0x0003a0  font: Isabelle
   1.503 +\<Sigma>                code: 0x0003a3  font: Isabelle
   1.504 +\<Upsilon>              code: 0x0003a5  font: Isabelle
   1.505 +\<Phi>                  code: 0x0003a6  font: Isabelle
   1.506 +\<Psi>                  code: 0x0003a8  font: Isabelle
   1.507 +\<Omega>                code: 0x0003a9  font: Isabelle
   1.508 +\<bool>                 code: 0x01d539  font: Isabelle
   1.509 +\<complex>              code: 0x002102  font: Isabelle
   1.510 +\<nat>                  code: 0x002115  font: Isabelle
   1.511 +\<rat>                  code: 0x00211a  font: Isabelle
   1.512 +\<real>                 code: 0x00211d  font: Isabelle
   1.513 +\<int>                  code: 0x002124  font: Isabelle
   1.514 +\<leftarrow>            code: 0x002190  font: Isabelle
   1.515 +\<longleftarrow>        code: 0x0027f5  font: Isabelle
   1.516 +\<rightarrow>           code: 0x002192  font: Isabelle
   1.517 +\<longrightarrow>       code: 0x0027f6  font: Isabelle
   1.518 +\<Leftarrow>            code: 0x0021d0  font: Isabelle
   1.519 +\<Longleftarrow>        code: 0x0027f8  font: Isabelle
   1.520 +\<Rightarrow>           code: 0x0021d2  font: Isabelle
   1.521 +\<Longrightarrow>       code: 0x0027f9  font: Isabelle
   1.522 +\<leftrightarrow>       code: 0x002194  font: Isabelle
   1.523 +\<longleftrightarrow>   code: 0x0027f7  font: Isabelle
   1.524 +\<Leftrightarrow>       code: 0x0021d4  font: Isabelle
   1.525 +\<Longleftrightarrow>   code: 0x0027fa  font: Isabelle
   1.526 +\<mapsto>               code: 0x0021a6  font: Isabelle
   1.527 +\<longmapsto>           code: 0x0027fc  font: Isabelle
   1.528 +\<midarrow>             code: 0x002500  font: Isabelle
   1.529 +\<Midarrow>             code: 0x002550  font: Isabelle
   1.530 +\<hookleftarrow>        code: 0x0021a9  font: Isabelle
   1.531 +\<hookrightarrow>       code: 0x0021aa  font: Isabelle
   1.532 +\<leftharpoondown>      code: 0x0021bd  font: Isabelle
   1.533 +\<rightharpoondown>     code: 0x0021c1  font: Isabelle
   1.534 +\<leftharpoonup>        code: 0x0021bc  font: Isabelle
   1.535 +\<rightharpoonup>       code: 0x0021c0  font: Isabelle
   1.536 +\<rightleftharpoons>    code: 0x0021cc  font: Isabelle
   1.537 +\<leadsto>              code: 0x00219d  font: Isabelle
   1.538 +\<downharpoonleft>      code: 0x0021c3  font: Isabelle
   1.539 +\<downharpoonright>     code: 0x0021c2  font: Isabelle
   1.540 +\<upharpoonleft>        code: 0x0021bf  font: Isabelle
   1.541 +\<upharpoonright>       code: 0x0021be  font: Isabelle
   1.542 +\<restriction>          code: 0x0021be  font: Isabelle
   1.543 +\<Colon>                code: 0x002237  font: Isabelle
   1.544 +\<up>                   code: 0x002191  font: Isabelle
   1.545 +\<Up>                   code: 0x0021d1  font: Isabelle
   1.546 +\<down>                 code: 0x002193  font: Isabelle
   1.547 +\<Down>                 code: 0x0021d3  font: Isabelle
   1.548 +\<updown>               code: 0x002195  font: Isabelle
   1.549 +\<Updown>               code: 0x0021d5  font: Isabelle
   1.550 +\<langle>               code: 0x0027e8  font: Isabelle
   1.551 +\<rangle>               code: 0x0027e9  font: Isabelle
   1.552 +\<lceil>                code: 0x002308  font: Isabelle
   1.553 +\<rceil>                code: 0x002309  font: Isabelle
   1.554 +\<lfloor>               code: 0x00230a  font: Isabelle
   1.555 +\<rfloor>               code: 0x00230b  font: Isabelle
   1.556 +\<lparr>                code: 0x002987  font: Isabelle
   1.557 +\<rparr>                code: 0x002988  font: Isabelle
   1.558 +\<lbrakk>               code: 0x0027e6  font: Isabelle
   1.559 +\<rbrakk>               code: 0x0027e7  font: Isabelle
   1.560 +\<lbrace>               code: 0x002983  font: Isabelle
   1.561 +\<rbrace>               code: 0x002984  font: Isabelle
   1.562 +\<guillemotleft>        code: 0x0000ab
   1.563 +\<guillemotright>       code: 0x0000bb
   1.564 +\<bottom>               code: 0x0022a5  font: Isabelle
   1.565 +\<top>                  code: 0x0022a4  font: Isabelle
   1.566 +\<and>                  code: 0x002227  font: Isabelle
   1.567 +\<And>                  code: 0x0022c0  font: Isabelle
   1.568 +\<or>                   code: 0x002228  font: Isabelle
   1.569 +\<Or>                   code: 0x0022c1  font: Isabelle
   1.570 +\<forall>               code: 0x002200  font: Isabelle
   1.571 +\<exists>               code: 0x002203  font: Isabelle
   1.572 +\<nexists>              code: 0x002204  font: Isabelle
   1.573 +\<not>                  code: 0x0000ac  font: Isabelle
   1.574 +\<box>                  code: 0x0025a1  font: Isabelle
   1.575 +\<diamond>              code: 0x0025c7  font: Isabelle
   1.576 +\<turnstile>            code: 0x0022a2  font: Isabelle
   1.577 +\<Turnstile>            code: 0x0022a8  font: Isabelle
   1.578 +\<tturnstile>           code: 0x0022a9  font: Isabelle
   1.579 +\<TTurnstile>           code: 0x0022ab  font: Isabelle
   1.580 +\<stileturn>            code: 0x0022a3  font: Isabelle
   1.581 +\<surd>                 code: 0x00221a  font: Isabelle
   1.582 +\<le>                   code: 0x002264  font: Isabelle
   1.583 +\<ge>                   code: 0x002265  font: Isabelle
   1.584 +\<lless>                code: 0x00226a  font: Isabelle
   1.585 +\<ggreater>             code: 0x00226b  font: Isabelle
   1.586 +\<lesssim>              code: 0x002272  font: Isabelle
   1.587 +\<greatersim>           code: 0x002273  font: Isabelle
   1.588 +\<lessapprox>           code: 0x002a85  font: Isabelle
   1.589 +\<greaterapprox>        code: 0x002a86  font: Isabelle
   1.590 +\<in>                   code: 0x002208  font: Isabelle
   1.591 +\<notin>                code: 0x002209  font: Isabelle
   1.592 +\<subset>               code: 0x002282  font: Isabelle
   1.593 +\<supset>               code: 0x002283  font: Isabelle
   1.594 +\<subseteq>             code: 0x002286  font: Isabelle
   1.595 +\<supseteq>             code: 0x002287  font: Isabelle
   1.596 +\<sqsubset>             code: 0x00228f  font: Isabelle
   1.597 +\<sqsupset>             code: 0x002290  font: Isabelle
   1.598 +\<sqsubseteq>           code: 0x002291  font: Isabelle
   1.599 +\<sqsupseteq>           code: 0x002292  font: Isabelle
   1.600 +\<inter>                code: 0x002229  font: Isabelle
   1.601 +\<Inter>                code: 0x0022c2  font: Isabelle
   1.602 +\<union>                code: 0x00222a  font: Isabelle
   1.603 +\<Union>                code: 0x0022c3  font: Isabelle
   1.604 +\<squnion>              code: 0x002294  font: Isabelle
   1.605 +\<Squnion>              code: 0x002a06  font: Isabelle
   1.606 +\<sqinter>              code: 0x002293  font: Isabelle
   1.607 +\<Sqinter>              code: 0x002a05  font: Isabelle
   1.608 +\<setminus>             code: 0x002216  font: Isabelle
   1.609 +\<propto>               code: 0x00221d  font: Isabelle
   1.610 +\<uplus>                code: 0x00228e  font: Isabelle
   1.611 +\<Uplus>                code: 0x002a04  font: Isabelle
   1.612 +\<noteq>                code: 0x002260  font: Isabelle
   1.613 +\<sim>                  code: 0x00223c  font: Isabelle
   1.614 +\<doteq>                code: 0x002250  font: Isabelle
   1.615 +\<simeq>                code: 0x002243  font: Isabelle
   1.616 +\<approx>               code: 0x002248  font: Isabelle
   1.617 +\<asymp>                code: 0x00224d  font: Isabelle
   1.618 +\<cong>                 code: 0x002245  font: Isabelle
   1.619 +\<smile>                code: 0x002323  font: Isabelle
   1.620 +\<equiv>                code: 0x002261  font: Isabelle
   1.621 +\<frown>                code: 0x002322  font: Isabelle
   1.622 +\<Join>                 code: 0x0022c8  font: Isabelle
   1.623 +\<bowtie>               code: 0x002a1d  font: Isabelle
   1.624 +\<prec>                 code: 0x00227a  font: Isabelle
   1.625 +\<succ>                 code: 0x00227b  font: Isabelle
   1.626 +\<preceq>               code: 0x00227c  font: Isabelle
   1.627 +\<succeq>               code: 0x00227d  font: Isabelle
   1.628 +\<parallel>             code: 0x002225  font: Isabelle
   1.629 +\<bar>                  code: 0x0000a6
   1.630 +\<plusminus>            code: 0x0000b1  font: Isabelle
   1.631 +\<minusplus>            code: 0x002213  font: Isabelle
   1.632 +\<times>                code: 0x0000d7  font: Isabelle
   1.633 +\<div>                  code: 0x0000f7  font: Isabelle
   1.634 +\<cdot>                 code: 0x0022c5  font: Isabelle
   1.635 +\<star>                 code: 0x0022c6  font: Isabelle
   1.636 +\<bullet>               code: 0x002219  font: Isabelle
   1.637 +\<circ>                 code: 0x002218  font: Isabelle
   1.638 +\<dagger>               code: 0x002020  font: Isabelle
   1.639 +\<ddagger>              code: 0x002021  font: Isabelle
   1.640 +\<lhd>                  code: 0x0022b2  font: Isabelle
   1.641 +\<rhd>                  code: 0x0022b3  font: Isabelle
   1.642 +\<unlhd>                code: 0x0022b4  font: Isabelle
   1.643 +\<unrhd>                code: 0x0022b5  font: Isabelle
   1.644 +\<triangleleft>         code: 0x0025c3  font: Isabelle
   1.645 +\<triangleright>        code: 0x0025b9  font: Isabelle
   1.646 +\<triangle>             code: 0x0025b3  font: Isabelle
   1.647 +\<triangleq>            code: 0x00225c  font: Isabelle
   1.648 +\<oplus>                code: 0x002295  font: Isabelle
   1.649 +\<Oplus>                code: 0x002a01  font: Isabelle
   1.650 +\<otimes>               code: 0x002297  font: Isabelle
   1.651 +\<Otimes>               code: 0x002a02  font: Isabelle
   1.652 +\<odot>                 code: 0x002299  font: Isabelle
   1.653 +\<Odot>                 code: 0x002a00  font: Isabelle
   1.654 +\<ominus>               code: 0x002296  font: Isabelle
   1.655 +\<oslash>               code: 0x002298  font: Isabelle
   1.656 +\<dots>                 code: 0x002026  font: Isabelle
   1.657 +\<cdots>                code: 0x0022ef  font: Isabelle
   1.658 +\<Sum>                  code: 0x002211  font: Isabelle
   1.659 +\<Prod>                 code: 0x00220f  font: Isabelle
   1.660 +\<Coprod>               code: 0x002210  font: Isabelle
   1.661 +\<infinity>             code: 0x00221e  font: Isabelle
   1.662 +\<integral>             code: 0x00222b  font: Isabelle
   1.663 +\<ointegral>            code: 0x00222e  font: Isabelle
   1.664 +\<clubsuit>             code: 0x002663  font: Isabelle
   1.665 +\<diamondsuit>          code: 0x002662  font: Isabelle
   1.666 +\<heartsuit>            code: 0x002661  font: Isabelle
   1.667 +\<spadesuit>            code: 0x002660  font: Isabelle
   1.668 +\<aleph>                code: 0x002135  font: Isabelle
   1.669 +\<emptyset>             code: 0x002205  font: Isabelle
   1.670 +\<nabla>                code: 0x002207  font: Isabelle
   1.671 +\<partial>              code: 0x002202  font: Isabelle
   1.672 +\<Re>                   code: 0x00211c  font: Isabelle
   1.673 +\<Im>                   code: 0x002111  font: Isabelle
   1.674 +\<flat>                 code: 0x00266d  font: Isabelle
   1.675 +\<natural>              code: 0x00266e  font: Isabelle
   1.676 +\<sharp>                code: 0x00266f  font: Isabelle
   1.677 +\<angle>                code: 0x002220  font: Isabelle
   1.678 +\<copyright>            code: 0x0000a9  font: Isabelle
   1.679 +\<registered>           code: 0x0000ae  font: Isabelle
   1.680 +\<hyphen>               code: 0x0000ad
   1.681 +\<inverse>              code: 0x0000af
   1.682 +\<onesuperior>          code: 0x0000b9
   1.683 +\<onequarter>           code: 0x0000bc
   1.684 +\<twosuperior>          code: 0x0000b2
   1.685 +\<onehalf>              code: 0x0000bd
   1.686 +\<threesuperior>        code: 0x0000b3
   1.687 +\<threequarters>        code: 0x0000be
   1.688 +\<ordfeminine>          code: 0x0000aa
   1.689 +\<ordmasculine>         code: 0x0000ba
   1.690 +\<section>              code: 0x0000a7
   1.691 +\<paragraph>            code: 0x0000b6
   1.692 +\<exclamdown>           code: 0x0000a1
   1.693 +\<questiondown>         code: 0x0000bf
   1.694 +\<euro>                 code: 0x0020ac  font: Isabelle
   1.695 +\<pounds>               code: 0x0000a3
   1.696 +\<yen>                  code: 0x0000a5
   1.697 +\<cent>                 code: 0x0000a2
   1.698 +\<currency>             code: 0x0000a4
   1.699 +\<degree>               code: 0x0000b0  font: Isabelle
   1.700 +\<amalg>                code: 0x002a3f  font: Isabelle
   1.701 +\<mho>                  code: 0x002127  font: Isabelle
   1.702 +\<lozenge>              code: 0x0025ca  font: Isabelle
   1.703 +\<wp>                   code: 0x002118  font: Isabelle
   1.704 +\<wrong>                code: 0x002240  font: Isabelle
   1.705 +\<struct>               code: 0x0022c4  font: Isabelle
   1.706 +\<acute>                code: 0x0000b4
   1.707 +\<index>                code: 0x000131  font: Isabelle
   1.708 +\<dieresis>             code: 0x0000a8
   1.709 +\<cedilla>              code: 0x0000b8
   1.710 +\<hungarumlaut>         code: 0x0002dd
   1.711 +\<spacespace>           code: 0x002423  font: Isabelle
   1.712 +\<some>                 code: 0x0003f5  font: Isabelle
   1.713