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