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