etc/symbols
author wenzelm
Sun Jun 19 14:11:06 2011 +0200 (2011-06-19)
changeset 43455 4b4b93672f15
parent 42244 15bba1fb39d1
child 43463 0a2ffb071fca
permissions -rw-r--r--
some unicode chars for special control symbols;
     1 # Default interpretation of some Isabelle symbols
     2 
     3 \<zero>                 code: 0x01d7ec  font: Isabelle
     4 \<one>                  code: 0x01d7ed  font: Isabelle
     5 \<two>                  code: 0x01d7ee  font: Isabelle
     6 \<three>                code: 0x01d7ef  font: Isabelle
     7 \<four>                 code: 0x01d7f0  font: Isabelle
     8 \<five>                 code: 0x01d7f1  font: Isabelle
     9 \<six>                  code: 0x01d7f2  font: Isabelle
    10 \<seven>                code: 0x01d7f3  font: Isabelle
    11 \<eight>                code: 0x01d7f4  font: Isabelle
    12 \<nine>                 code: 0x01d7f5  font: Isabelle
    13 \<A>                    code: 0x01d49c  font: Isabelle
    14 \<B>                    code: 0x00212c  font: Isabelle
    15 \<C>                    code: 0x01d49e  font: Isabelle
    16 \<D>                    code: 0x01d49f  font: Isabelle
    17 \<E>                    code: 0x002130  font: Isabelle
    18 \<F>                    code: 0x002131  font: Isabelle
    19 \<G>                    code: 0x01d4a2  font: Isabelle
    20 \<H>                    code: 0x00210b  font: Isabelle
    21 \<I>                    code: 0x002110  font: Isabelle
    22 \<J>                    code: 0x01d4a5  font: Isabelle
    23 \<K>                    code: 0x01d4a6  font: Isabelle
    24 \<L>                    code: 0x002112  font: Isabelle
    25 \<M>                    code: 0x002133  font: Isabelle
    26 \<N>                    code: 0x01d4a9  font: Isabelle
    27 \<O>                    code: 0x01d4aa  font: Isabelle
    28 \<P>                    code: 0x01d4ab  font: Isabelle
    29 \<Q>                    code: 0x01d4ac  font: Isabelle
    30 \<R>                    code: 0x00211b  font: Isabelle
    31 \<S>                    code: 0x01d4ae  font: Isabelle
    32 \<T>                    code: 0x01d4af  font: Isabelle
    33 \<U>                    code: 0x01d4b0  font: Isabelle
    34 \<V>                    code: 0x01d4b1  font: Isabelle
    35 \<W>                    code: 0x01d4b2  font: Isabelle
    36 \<X>                    code: 0x01d4b3  font: Isabelle
    37 \<Y>                    code: 0x01d4b4  font: Isabelle
    38 \<Z>                    code: 0x01d4b5  font: Isabelle
    39 \<a>                    code: 0x01d5ba  font: Isabelle
    40 \<b>                    code: 0x01d5bb  font: Isabelle
    41 \<c>                    code: 0x01d5bc  font: Isabelle
    42 \<d>                    code: 0x01d5bd  font: Isabelle
    43 \<e>                    code: 0x01d5be  font: Isabelle
    44 \<f>                    code: 0x01d5bf  font: Isabelle
    45 \<g>                    code: 0x01d5c0  font: Isabelle
    46 \<h>                    code: 0x01d5c1  font: Isabelle
    47 \<i>                    code: 0x01d5c2  font: Isabelle
    48 \<j>                    code: 0x01d5c3  font: Isabelle
    49 \<k>                    code: 0x01d5c4  font: Isabelle
    50 \<l>                    code: 0x01d5c5  font: Isabelle
    51 \<m>                    code: 0x01d5c6  font: Isabelle
    52 \<n>                    code: 0x01d5c7  font: Isabelle
    53 \<o>                    code: 0x01d5c8  font: Isabelle
    54 \<p>                    code: 0x01d5c9  font: Isabelle
    55 \<q>                    code: 0x01d5ca  font: Isabelle
    56 \<r>                    code: 0x01d5cb  font: Isabelle
    57 \<s>                    code: 0x01d5cc  font: Isabelle
    58 \<t>                    code: 0x01d5cd  font: Isabelle
    59 \<u>                    code: 0x01d5ce  font: Isabelle
    60 \<v>                    code: 0x01d5cf  font: Isabelle
    61 \<w>                    code: 0x01d5d0  font: Isabelle
    62 \<x>                    code: 0x01d5d1  font: Isabelle
    63 \<y>                    code: 0x01d5d2  font: Isabelle
    64 \<z>                    code: 0x01d5d3  font: Isabelle
    65 \<AA>                   code: 0x01d504  font: Isabelle
    66 \<BB>                   code: 0x01d505  font: Isabelle
    67 \<CC>                   code: 0x00212d  font: Isabelle
    68 \<DD>                   code: 0x01d507  font: Isabelle
    69 \<EE>                   code: 0x01d508  font: Isabelle
    70 \<FF>                   code: 0x01d509  font: Isabelle
    71 \<GG>                   code: 0x01d50a  font: Isabelle
    72 \<HH>                   code: 0x00210c  font: Isabelle
    73 #\<II>                   code: 0x01d50c  font: Isabelle
    74 \<JJ>                   code: 0x01d50d  font: Isabelle
    75 \<KK>                   code: 0x01d50e  font: Isabelle
    76 \<LL>                   code: 0x01d50f  font: Isabelle
    77 \<MM>                   code: 0x01d510  font: Isabelle
    78 \<NN>                   code: 0x01d511  font: Isabelle
    79 \<OO>                   code: 0x01d512  font: Isabelle
    80 \<PP>                   code: 0x01d513  font: Isabelle
    81 \<QQ>                   code: 0x01d514  font: Isabelle
    82 #\<RR>                   code: 0x01d515  font: Isabelle
    83 \<SS>                   code: 0x01d516  font: Isabelle
    84 \<TT>                   code: 0x01d517  font: Isabelle
    85 \<UU>                   code: 0x01d518  font: Isabelle
    86 \<VV>                   code: 0x01d519  font: Isabelle
    87 \<WW>                   code: 0x01d51a  font: Isabelle
    88 \<XX>                   code: 0x01d51b  font: Isabelle
    89 \<YY>                   code: 0x01d51c  font: Isabelle
    90 \<ZZ>                   code: 0x002128  font: Isabelle
    91 \<aa>                   code: 0x01d51e  font: Isabelle
    92 \<bb>                   code: 0x01d51f  font: Isabelle
    93 \<cc>                   code: 0x01d520  font: Isabelle
    94 \<dd>                   code: 0x01d521  font: Isabelle
    95 \<ee>                   code: 0x01d522  font: Isabelle
    96 \<ff>                   code: 0x01d523  font: Isabelle
    97 \<gg>                   code: 0x01d524  font: Isabelle
    98 \<hh>                   code: 0x01d525  font: Isabelle
    99 \<ii>                   code: 0x01d526  font: Isabelle
   100 \<jj>                   code: 0x01d527  font: Isabelle
   101 \<kk>                   code: 0x01d528  font: Isabelle
   102 \<ll>                   code: 0x01d529  font: Isabelle
   103 \<mm>                   code: 0x01d52a  font: Isabelle
   104 \<nn>                   code: 0x01d52b  font: Isabelle
   105 \<oo>                   code: 0x01d52c  font: Isabelle
   106 \<pp>                   code: 0x01d52d  font: Isabelle
   107 \<qq>                   code: 0x01d52e  font: Isabelle
   108 \<rr>                   code: 0x01d52f  font: Isabelle
   109 \<ss>                   code: 0x01d530  font: Isabelle
   110 \<tt>                   code: 0x01d531  font: Isabelle
   111 \<uu>                   code: 0x01d532  font: Isabelle
   112 \<vv>                   code: 0x01d533  font: Isabelle
   113 \<ww>                   code: 0x01d534  font: Isabelle
   114 \<xx>                   code: 0x01d535  font: Isabelle
   115 \<yy>                   code: 0x01d536  font: Isabelle
   116 \<zz>                   code: 0x01d537  font: Isabelle
   117 \<alpha>                code: 0x0003b1  font: Isabelle
   118 \<beta>                 code: 0x0003b2  font: Isabelle
   119 \<gamma>                code: 0x0003b3  font: Isabelle
   120 \<delta>                code: 0x0003b4  font: Isabelle
   121 \<epsilon>              code: 0x0003b5  font: Isabelle
   122 \<zeta>                 code: 0x0003b6  font: Isabelle
   123 \<eta>                  code: 0x0003b7  font: Isabelle
   124 \<theta>                code: 0x0003b8  font: Isabelle
   125 \<iota>                 code: 0x0003b9  font: Isabelle
   126 \<kappa>                code: 0x0003ba  font: Isabelle
   127 \<lambda>               code: 0x0003bb  font: Isabelle  abbrev: %
   128 \<mu>                   code: 0x0003bc  font: Isabelle
   129 \<nu>                   code: 0x0003bd  font: Isabelle
   130 \<xi>                   code: 0x0003be  font: Isabelle
   131 \<pi>                   code: 0x0003c0  font: Isabelle
   132 \<rho>                  code: 0x0003c1  font: Isabelle
   133 \<sigma>                code: 0x0003c3  font: Isabelle
   134 \<tau>                  code: 0x0003c4  font: Isabelle
   135 \<upsilon>              code: 0x0003c5  font: Isabelle
   136 \<phi>                  code: 0x0003c6  font: Isabelle
   137 \<chi>                  code: 0x0003c7  font: Isabelle
   138 \<psi>                  code: 0x0003c8  font: Isabelle
   139 \<omega>                code: 0x0003c9  font: Isabelle
   140 \<Gamma>                code: 0x000393  font: Isabelle
   141 \<Delta>                code: 0x000394  font: Isabelle
   142 \<Theta>                code: 0x000398  font: Isabelle
   143 \<Lambda>               code: 0x00039b  font: Isabelle
   144 \<Xi>                   code: 0x00039e  font: Isabelle
   145 \<Pi>                   code: 0x0003a0  font: Isabelle
   146 \<Sigma>                code: 0x0003a3  font: Isabelle
   147 \<Upsilon>              code: 0x0003a5  font: Isabelle
   148 \<Phi>                  code: 0x0003a6  font: Isabelle
   149 \<Psi>                  code: 0x0003a8  font: Isabelle
   150 \<Omega>                code: 0x0003a9  font: Isabelle
   151 \<bool>                 code: 0x01d539  font: Isabelle
   152 \<complex>              code: 0x002102  font: Isabelle
   153 \<nat>                  code: 0x002115  font: Isabelle
   154 \<rat>                  code: 0x00211a  font: Isabelle
   155 \<real>                 code: 0x00211d  font: Isabelle
   156 \<int>                  code: 0x002124  font: Isabelle
   157 \<leftarrow>            code: 0x002190  font: Isabelle
   158 \<longleftarrow>        code: 0x0027f5  font: Isabelle
   159 \<rightarrow>           code: 0x002192  font: Isabelle  abbrev: ->
   160 \<longrightarrow>       code: 0x0027f6  font: Isabelle  abbrev: -->
   161 \<Leftarrow>            code: 0x0021d0  font: Isabelle
   162 \<Longleftarrow>        code: 0x0027f8  font: Isabelle 
   163 \<Rightarrow>           code: 0x0021d2  font: Isabelle  abbrev: =>
   164 \<Longrightarrow>       code: 0x0027f9  font: Isabelle  abbrev: ==>
   165 \<leftrightarrow>       code: 0x002194  font: Isabelle
   166 \<longleftrightarrow>   code: 0x0027f7  font: Isabelle  abbrev: <->
   167 \<Leftrightarrow>       code: 0x0021d4  font: Isabelle
   168 \<Longleftrightarrow>   code: 0x0027fa  font: Isabelle  abbrev: <=>
   169 \<mapsto>               code: 0x0021a6  font: Isabelle  abbrev: |->
   170 \<longmapsto>           code: 0x0027fc  font: Isabelle  abbrev: |-->
   171 \<midarrow>             code: 0x002500  font: Isabelle
   172 \<Midarrow>             code: 0x002550  font: Isabelle
   173 \<hookleftarrow>        code: 0x0021a9  font: Isabelle
   174 \<hookrightarrow>       code: 0x0021aa  font: Isabelle
   175 \<leftharpoondown>      code: 0x0021bd  font: Isabelle
   176 \<rightharpoondown>     code: 0x0021c1  font: Isabelle
   177 \<leftharpoonup>        code: 0x0021bc  font: Isabelle
   178 \<rightharpoonup>       code: 0x0021c0  font: Isabelle
   179 \<rightleftharpoons>    code: 0x0021cc  font: Isabelle
   180 \<leadsto>              code: 0x00219d  font: Isabelle  abbrev: ~>
   181 \<downharpoonleft>      code: 0x0021c3  font: Isabelle
   182 \<downharpoonright>     code: 0x0021c2  font: Isabelle
   183 \<upharpoonleft>        code: 0x0021bf  font: Isabelle
   184 #\<upharpoonright>       code: 0x0021be  font: Isabelle
   185 \<restriction>          code: 0x0021be  font: Isabelle
   186 \<Colon>                code: 0x002237  font: Isabelle
   187 \<up>                   code: 0x002191  font: Isabelle
   188 \<Up>                   code: 0x0021d1  font: Isabelle
   189 \<down>                 code: 0x002193  font: Isabelle
   190 \<Down>                 code: 0x0021d3  font: Isabelle
   191 \<updown>               code: 0x002195  font: Isabelle
   192 \<Updown>               code: 0x0021d5  font: Isabelle
   193 \<langle>               code: 0x0027e8  font: Isabelle  abbrev: <.
   194 \<rangle>               code: 0x0027e9  font: Isabelle  abbrev: .>
   195 \<lceil>                code: 0x002308  font: Isabelle
   196 \<rceil>                code: 0x002309  font: Isabelle
   197 \<lfloor>               code: 0x00230a  font: Isabelle
   198 \<rfloor>               code: 0x00230b  font: Isabelle
   199 \<lparr>                code: 0x002987  font: Isabelle  abbrev: (|
   200 \<rparr>                code: 0x002988  font: Isabelle  abbrev: |)
   201 \<lbrakk>               code: 0x0027e6  font: Isabelle  abbrev: [|
   202 \<rbrakk>               code: 0x0027e7  font: Isabelle  abbrev: |]
   203 \<lbrace>               code: 0x002983  font: Isabelle  abbrev: {.
   204 \<rbrace>               code: 0x002984  font: Isabelle  abbrev: .}
   205 \<guillemotleft>        code: 0x0000ab                  abbrev: <<
   206 \<guillemotright>       code: 0x0000bb                  abbrev: >>
   207 \<bottom>               code: 0x0022a5  font: Isabelle
   208 \<top>                  code: 0x0022a4  font: Isabelle
   209 \<and>                  code: 0x002227  font: Isabelle  abbrev: /\
   210 \<And>                  code: 0x0022c0  font: Isabelle  abbrev: !!
   211 \<or>                   code: 0x002228  font: Isabelle  abbrev: \/
   212 \<Or>                   code: 0x0022c1  font: Isabelle  abbrev: ??
   213 \<forall>               code: 0x002200  font: Isabelle  abbrev: !
   214 \<exists>               code: 0x002203  font: Isabelle  abbrev: ?
   215 \<nexists>              code: 0x002204  font: Isabelle  abbrev: ~?
   216 \<not>                  code: 0x0000ac  font: Isabelle  abbrev: ~
   217 \<box>                  code: 0x0025a1  font: Isabelle
   218 \<diamond>              code: 0x0025c7  font: Isabelle
   219 \<turnstile>            code: 0x0022a2  font: Isabelle  abbrev: |-
   220 \<Turnstile>            code: 0x0022a8  font: Isabelle  abbrev: |=
   221 \<tturnstile>           code: 0x0022a9  font: Isabelle  abbrev: ||-
   222 \<TTurnstile>           code: 0x0022ab  font: Isabelle  abbrev: ||=
   223 \<stileturn>            code: 0x0022a3  font: Isabelle  abbrev: -|
   224 \<surd>                 code: 0x00221a  font: Isabelle
   225 \<le>                   code: 0x002264  font: Isabelle  abbrev: <=
   226 \<ge>                   code: 0x002265  font: Isabelle  abbrev: >=
   227 \<lless>                code: 0x00226a  font: Isabelle
   228 \<ggreater>             code: 0x00226b  font: Isabelle
   229 \<lesssim>              code: 0x002272  font: Isabelle
   230 \<greatersim>           code: 0x002273  font: Isabelle
   231 \<lessapprox>           code: 0x002a85  font: Isabelle
   232 \<greaterapprox>        code: 0x002a86  font: Isabelle
   233 \<in>                   code: 0x002208  font: Isabelle  abbrev: :
   234 \<notin>                code: 0x002209  font: Isabelle  abbrev: ~:
   235 \<subset>               code: 0x002282  font: Isabelle
   236 \<supset>               code: 0x002283  font: Isabelle
   237 \<subseteq>             code: 0x002286  font: Isabelle  abbrev: (=
   238 \<supseteq>             code: 0x002287  font: Isabelle  abbrev: =)
   239 \<sqsubset>             code: 0x00228f  font: Isabelle
   240 \<sqsupset>             code: 0x002290  font: Isabelle
   241 \<sqsubseteq>           code: 0x002291  font: Isabelle  abbrev: [=
   242 \<sqsupseteq>           code: 0x002292  font: Isabelle  abbrev: =]
   243 \<inter>                code: 0x002229  font: Isabelle  abbrev: Int
   244 \<Inter>                code: 0x0022c2  font: Isabelle  abbrev: Inter
   245 \<union>                code: 0x00222a  font: Isabelle  abbrev: Un
   246 \<Union>                code: 0x0022c3  font: Isabelle  abbrev: Union
   247 \<squnion>              code: 0x002294  font: Isabelle
   248 \<Squnion>              code: 0x002a06  font: Isabelle
   249 \<sqinter>              code: 0x002293  font: Isabelle
   250 \<Sqinter>              code: 0x002a05  font: Isabelle
   251 \<setminus>             code: 0x002216  font: Isabelle
   252 \<propto>               code: 0x00221d  font: Isabelle
   253 \<uplus>                code: 0x00228e  font: Isabelle
   254 \<Uplus>                code: 0x002a04  font: Isabelle
   255 \<noteq>                code: 0x002260  font: Isabelle  abbrev: ~=
   256 \<sim>                  code: 0x00223c  font: Isabelle
   257 \<doteq>                code: 0x002250  font: Isabelle
   258 \<simeq>                code: 0x002243  font: Isabelle
   259 \<approx>               code: 0x002248  font: Isabelle
   260 \<asymp>                code: 0x00224d  font: Isabelle
   261 \<cong>                 code: 0x002245  font: Isabelle
   262 \<smile>                code: 0x002323  font: Isabelle
   263 \<equiv>                code: 0x002261  font: Isabelle  abbrev: ==
   264 \<frown>                code: 0x002322  font: Isabelle
   265 \<Join>                 code: 0x0022c8  font: Isabelle
   266 \<bowtie>               code: 0x002a1d  font: Isabelle
   267 \<prec>                 code: 0x00227a  font: Isabelle
   268 \<succ>                 code: 0x00227b  font: Isabelle
   269 \<preceq>               code: 0x00227c  font: Isabelle
   270 \<succeq>               code: 0x00227d  font: Isabelle
   271 \<parallel>             code: 0x002225  font: Isabelle  abbrev: ||
   272 \<bar>                  code: 0x0000a6
   273 \<plusminus>            code: 0x0000b1  font: Isabelle
   274 \<minusplus>            code: 0x002213  font: Isabelle
   275 \<times>                code: 0x0000d7  font: Isabelle
   276 \<div>                  code: 0x0000f7  font: Isabelle
   277 \<cdot>                 code: 0x0022c5  font: Isabelle
   278 \<star>                 code: 0x0022c6  font: Isabelle
   279 \<bullet>               code: 0x002219  font: Isabelle
   280 \<circ>                 code: 0x002218  font: Isabelle
   281 \<dagger>               code: 0x002020  font: Isabelle
   282 \<ddagger>              code: 0x002021  font: Isabelle
   283 \<lhd>                  code: 0x0022b2  font: Isabelle
   284 \<rhd>                  code: 0x0022b3  font: Isabelle
   285 \<unlhd>                code: 0x0022b4  font: Isabelle
   286 \<unrhd>                code: 0x0022b5  font: Isabelle
   287 \<triangleleft>         code: 0x0025c3  font: Isabelle
   288 \<triangleright>        code: 0x0025b9  font: Isabelle
   289 \<triangle>             code: 0x0025b3  font: Isabelle
   290 \<triangleq>            code: 0x00225c  font: Isabelle
   291 \<oplus>                code: 0x002295  font: Isabelle  abbrev: +o
   292 \<Oplus>                code: 0x002a01  font: Isabelle  abbrev: +O
   293 \<otimes>               code: 0x002297  font: Isabelle  abbrev: *o
   294 \<Otimes>               code: 0x002a02  font: Isabelle  abbrev: *O
   295 \<odot>                 code: 0x002299  font: Isabelle  abbrev: .o
   296 \<Odot>                 code: 0x002a00  font: Isabelle  abbrev: .O
   297 \<ominus>               code: 0x002296  font: Isabelle  abbrev: -o
   298 \<oslash>               code: 0x002298  font: Isabelle  abbrev: /o
   299 \<dots>                 code: 0x002026  font: Isabelle  abbrev: ...
   300 \<cdots>                code: 0x0022ef  font: Isabelle
   301 \<Sum>                  code: 0x002211  font: Isabelle  abbrev: SUM
   302 \<Prod>                 code: 0x00220f  font: Isabelle  abbrev: PROD
   303 \<Coprod>               code: 0x002210  font: Isabelle
   304 \<infinity>             code: 0x00221e  font: Isabelle
   305 \<integral>             code: 0x00222b  font: Isabelle
   306 \<ointegral>            code: 0x00222e  font: Isabelle
   307 \<clubsuit>             code: 0x002663  font: Isabelle
   308 \<diamondsuit>          code: 0x002662  font: Isabelle
   309 \<heartsuit>            code: 0x002661  font: Isabelle
   310 \<spadesuit>            code: 0x002660  font: Isabelle
   311 \<aleph>                code: 0x002135  font: Isabelle
   312 \<emptyset>             code: 0x002205  font: Isabelle
   313 \<nabla>                code: 0x002207  font: Isabelle
   314 \<partial>              code: 0x002202  font: Isabelle
   315 \<Re>                   code: 0x00211c  font: Isabelle
   316 \<Im>                   code: 0x002111  font: Isabelle
   317 \<flat>                 code: 0x00266d  font: Isabelle
   318 \<natural>              code: 0x00266e  font: Isabelle
   319 \<sharp>                code: 0x00266f  font: Isabelle
   320 \<angle>                code: 0x002220  font: Isabelle
   321 \<copyright>            code: 0x0000a9  font: Isabelle
   322 \<registered>           code: 0x0000ae  font: Isabelle
   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  font: Isabelle
   343 \<amalg>                code: 0x002a3f  font: Isabelle
   344 \<mho>                  code: 0x002127  font: Isabelle
   345 \<lozenge>              code: 0x0025ca  font: Isabelle
   346 \<wp>                   code: 0x002118  font: Isabelle
   347 \<wrong>                code: 0x002240  font: Isabelle
   348 \<struct>               code: 0x0022c4  font: Isabelle
   349 \<acute>                code: 0x0000b4
   350 \<index>                code: 0x000131  font: Isabelle
   351 \<dieresis>             code: 0x0000a8
   352 \<cedilla>              code: 0x0000b8
   353 \<hungarumlaut>         code: 0x0002dd
   354 \<spacespace>           code: 0x002423  font: Isabelle
   355 \<some>                 code: 0x0003f5  font: Isabelle
   356 \<^sub>                 code: 0x0021e9
   357 \<^sup>                 code: 0x0021e7
   358 \<^isub>                code: 0x0021e3
   359 \<^isup>                code: 0x0021e1
   360 \<^bold>                code: 0x002759
   361