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