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