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