author bulwahn
Thu, 07 Jul 2011 23:33:14 +0200
changeset 43704 47b0be18ccbe
parent 43503 ca87677d2265
child 46213 0a5af667dc75
permissions -rw-r--r--
floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling

# Default interpretation of some Isabelle symbols

\<zero>                 code: 0x01d7ec
\<one>                  code: 0x01d7ed
\<two>                  code: 0x01d7ee
\<three>                code: 0x01d7ef
\<four>                 code: 0x01d7f0
\<five>                 code: 0x01d7f1
\<six>                  code: 0x01d7f2
\<seven>                code: 0x01d7f3
\<eight>                code: 0x01d7f4
\<nine>                 code: 0x01d7f5
\<A>                    code: 0x01d49c
\<B>                    code: 0x00212c
\<C>                    code: 0x01d49e
\<D>                    code: 0x01d49f
\<E>                    code: 0x002130
\<F>                    code: 0x002131
\<G>                    code: 0x01d4a2
\<H>                    code: 0x00210b
\<I>                    code: 0x002110
\<J>                    code: 0x01d4a5
\<K>                    code: 0x01d4a6
\<L>                    code: 0x002112
\<M>                    code: 0x002133
\<N>                    code: 0x01d4a9
\<O>                    code: 0x01d4aa
\<P>                    code: 0x01d4ab
\<Q>                    code: 0x01d4ac
\<R>                    code: 0x00211b
\<S>                    code: 0x01d4ae
\<T>                    code: 0x01d4af
\<U>                    code: 0x01d4b0
\<V>                    code: 0x01d4b1
\<W>                    code: 0x01d4b2
\<X>                    code: 0x01d4b3
\<Y>                    code: 0x01d4b4
\<Z>                    code: 0x01d4b5
\<a>                    code: 0x01d5ba
\<b>                    code: 0x01d5bb
\<c>                    code: 0x01d5bc
\<d>                    code: 0x01d5bd
\<e>                    code: 0x01d5be
\<f>                    code: 0x01d5bf
\<g>                    code: 0x01d5c0
\<h>                    code: 0x01d5c1
\<i>                    code: 0x01d5c2
\<j>                    code: 0x01d5c3
\<k>                    code: 0x01d5c4
\<l>                    code: 0x01d5c5
\<m>                    code: 0x01d5c6
\<n>                    code: 0x01d5c7
\<o>                    code: 0x01d5c8
\<p>                    code: 0x01d5c9
\<q>                    code: 0x01d5ca
\<r>                    code: 0x01d5cb
\<s>                    code: 0x01d5cc
\<t>                    code: 0x01d5cd
\<u>                    code: 0x01d5ce
\<v>                    code: 0x01d5cf
\<w>                    code: 0x01d5d0
\<x>                    code: 0x01d5d1
\<y>                    code: 0x01d5d2
\<z>                    code: 0x01d5d3
\<AA>                   code: 0x01d504
\<BB>                   code: 0x01d505
\<CC>                   code: 0x00212d
\<DD>                   code: 0x01d507
\<EE>                   code: 0x01d508
\<FF>                   code: 0x01d509
\<GG>                   code: 0x01d50a
\<HH>                   code: 0x00210c
#\<II>                   code: 0x01d50c
\<JJ>                   code: 0x01d50d
\<KK>                   code: 0x01d50e
\<LL>                   code: 0x01d50f
\<MM>                   code: 0x01d510
\<NN>                   code: 0x01d511
\<OO>                   code: 0x01d512
\<PP>                   code: 0x01d513
\<QQ>                   code: 0x01d514
#\<RR>                   code: 0x01d515
\<SS>                   code: 0x01d516
\<TT>                   code: 0x01d517
\<UU>                   code: 0x01d518
\<VV>                   code: 0x01d519
\<WW>                   code: 0x01d51a
\<XX>                   code: 0x01d51b
\<YY>                   code: 0x01d51c
\<ZZ>                   code: 0x002128
\<aa>                   code: 0x01d51e
\<bb>                   code: 0x01d51f
\<cc>                   code: 0x01d520
\<dd>                   code: 0x01d521
\<ee>                   code: 0x01d522
\<ff>                   code: 0x01d523
\<gg>                   code: 0x01d524
\<hh>                   code: 0x01d525
\<ii>                   code: 0x01d526
\<jj>                   code: 0x01d527
\<kk>                   code: 0x01d528
\<ll>                   code: 0x01d529
\<mm>                   code: 0x01d52a
\<nn>                   code: 0x01d52b
\<oo>                   code: 0x01d52c
\<pp>                   code: 0x01d52d
\<qq>                   code: 0x01d52e
\<rr>                   code: 0x01d52f
\<ss>                   code: 0x01d530
\<tt>                   code: 0x01d531
\<uu>                   code: 0x01d532
\<vv>                   code: 0x01d533
\<ww>                   code: 0x01d534
\<xx>                   code: 0x01d535
\<yy>                   code: 0x01d536
\<zz>                   code: 0x01d537
\<alpha>                code: 0x0003b1
\<beta>                 code: 0x0003b2
\<gamma>                code: 0x0003b3
\<delta>                code: 0x0003b4
\<epsilon>              code: 0x0003b5
\<zeta>                 code: 0x0003b6
\<eta>                  code: 0x0003b7
\<theta>                code: 0x0003b8
\<iota>                 code: 0x0003b9
\<kappa>                code: 0x0003ba
\<lambda>               code: 0x0003bb  abbrev: %
\<mu>                   code: 0x0003bc
\<nu>                   code: 0x0003bd
\<xi>                   code: 0x0003be
\<pi>                   code: 0x0003c0
\<rho>                  code: 0x0003c1
\<sigma>                code: 0x0003c3
\<tau>                  code: 0x0003c4
\<upsilon>              code: 0x0003c5
\<phi>                  code: 0x0003c6
\<chi>                  code: 0x0003c7
\<psi>                  code: 0x0003c8
\<omega>                code: 0x0003c9
\<Gamma>                code: 0x000393
\<Delta>                code: 0x000394
\<Theta>                code: 0x000398
\<Lambda>               code: 0x00039b
\<Xi>                   code: 0x00039e
\<Pi>                   code: 0x0003a0
\<Sigma>                code: 0x0003a3
\<Upsilon>              code: 0x0003a5
\<Phi>                  code: 0x0003a6
\<Psi>                  code: 0x0003a8
\<Omega>                code: 0x0003a9
\<bool>                 code: 0x01d539
\<complex>              code: 0x002102
\<nat>                  code: 0x002115
\<rat>                  code: 0x00211a
\<real>                 code: 0x00211d
\<int>                  code: 0x002124
\<leftarrow>            code: 0x002190
\<longleftarrow>        code: 0x0027f5
\<rightarrow>           code: 0x002192  abbrev: ->
\<longrightarrow>       code: 0x0027f6  abbrev: -->
\<Leftarrow>            code: 0x0021d0
\<Longleftarrow>        code: 0x0027f8
\<Rightarrow>           code: 0x0021d2  abbrev: =>
\<Longrightarrow>       code: 0x0027f9  abbrev: ==>
\<leftrightarrow>       code: 0x002194
\<longleftrightarrow>   code: 0x0027f7  abbrev: <->
\<Leftrightarrow>       code: 0x0021d4
\<Longleftrightarrow>   code: 0x0027fa  abbrev: <=>
\<mapsto>               code: 0x0021a6  abbrev: |->
\<longmapsto>           code: 0x0027fc  abbrev: |-->
\<midarrow>             code: 0x002500
\<Midarrow>             code: 0x002550
\<hookleftarrow>        code: 0x0021a9
\<hookrightarrow>       code: 0x0021aa
\<leftharpoondown>      code: 0x0021bd
\<rightharpoondown>     code: 0x0021c1
\<leftharpoonup>        code: 0x0021bc
\<rightharpoonup>       code: 0x0021c0
\<rightleftharpoons>    code: 0x0021cc
\<leadsto>              code: 0x00219d  abbrev: ~>
\<downharpoonleft>      code: 0x0021c3
\<downharpoonright>     code: 0x0021c2
\<upharpoonleft>        code: 0x0021bf
#\<upharpoonright>       code: 0x0021be
\<restriction>          code: 0x0021be
\<Colon>                code: 0x002237
\<up>                   code: 0x002191
\<Up>                   code: 0x0021d1
\<down>                 code: 0x002193
\<Down>                 code: 0x0021d3
\<updown>               code: 0x002195
\<Updown>               code: 0x0021d5
\<langle>               code: 0x0027e8  abbrev: <.
\<rangle>               code: 0x0027e9  abbrev: .>
\<lceil>                code: 0x002308
\<rceil>                code: 0x002309
\<lfloor>               code: 0x00230a
\<rfloor>               code: 0x00230b
\<lparr>                code: 0x002987  abbrev: (|
\<rparr>                code: 0x002988  abbrev: |)
\<lbrakk>               code: 0x0027e6  abbrev: [|
\<rbrakk>               code: 0x0027e7  abbrev: |]
\<lbrace>               code: 0x002983  abbrev: {.
\<rbrace>               code: 0x002984  abbrev: .}
\<guillemotleft>        code: 0x0000ab  abbrev: <<
\<guillemotright>       code: 0x0000bb  abbrev: >>
\<bottom>               code: 0x0022a5
\<top>                  code: 0x0022a4
\<and>                  code: 0x002227  abbrev: /\
\<And>                  code: 0x0022c0  abbrev: !!
\<or>                   code: 0x002228  abbrev: \/
\<Or>                   code: 0x0022c1  abbrev: ??
\<forall>               code: 0x002200  abbrev: !
\<exists>               code: 0x002203  abbrev: ?
\<nexists>              code: 0x002204  abbrev: ~?
\<not>                  code: 0x0000ac  abbrev: ~
\<box>                  code: 0x0025a1
\<diamond>              code: 0x0025c7
\<turnstile>            code: 0x0022a2  abbrev: |-
\<Turnstile>            code: 0x0022a8  abbrev: |=
\<tturnstile>           code: 0x0022a9  abbrev: ||-
\<TTurnstile>           code: 0x0022ab  abbrev: ||=
\<stileturn>            code: 0x0022a3  abbrev: -|
\<surd>                 code: 0x00221a
\<le>                   code: 0x002264  abbrev: <=
\<ge>                   code: 0x002265  abbrev: >=
\<lless>                code: 0x00226a
\<ggreater>             code: 0x00226b
\<lesssim>              code: 0x002272
\<greatersim>           code: 0x002273
\<lessapprox>           code: 0x002a85
\<greaterapprox>        code: 0x002a86
\<in>                   code: 0x002208  abbrev: :
\<notin>                code: 0x002209  abbrev: ~:
\<subset>               code: 0x002282
\<supset>               code: 0x002283
\<subseteq>             code: 0x002286  abbrev: (=
\<supseteq>             code: 0x002287  abbrev: =)
\<sqsubset>             code: 0x00228f
\<sqsupset>             code: 0x002290
\<sqsubseteq>           code: 0x002291  abbrev: [=
\<sqsupseteq>           code: 0x002292  abbrev: =]
\<inter>                code: 0x002229  abbrev: Int
\<Inter>                code: 0x0022c2  abbrev: Inter
\<union>                code: 0x00222a  abbrev: Un
\<Union>                code: 0x0022c3  abbrev: Union
\<squnion>              code: 0x002294
\<Squnion>              code: 0x002a06
\<sqinter>              code: 0x002293
\<Sqinter>              code: 0x002a05
\<setminus>             code: 0x002216
\<propto>               code: 0x00221d
\<uplus>                code: 0x00228e
\<Uplus>                code: 0x002a04
\<noteq>                code: 0x002260  abbrev: ~=
\<sim>                  code: 0x00223c
\<doteq>                code: 0x002250
\<simeq>                code: 0x002243
\<approx>               code: 0x002248
\<asymp>                code: 0x00224d
\<cong>                 code: 0x002245
\<smile>                code: 0x002323
\<equiv>                code: 0x002261  abbrev: ==
\<frown>                code: 0x002322
\<Join>                 code: 0x0022c8
\<bowtie>               code: 0x002a1d
\<prec>                 code: 0x00227a
\<succ>                 code: 0x00227b
\<preceq>               code: 0x00227c
\<succeq>               code: 0x00227d
\<parallel>             code: 0x002225  abbrev: ||
\<bar>                  code: 0x0000a6
\<plusminus>            code: 0x0000b1
\<minusplus>            code: 0x002213
\<times>                code: 0x0000d7
\<div>                  code: 0x0000f7
\<cdot>                 code: 0x0022c5
\<star>                 code: 0x0022c6
\<bullet>               code: 0x002219
\<circ>                 code: 0x002218
\<dagger>               code: 0x002020
\<ddagger>              code: 0x002021
\<lhd>                  code: 0x0022b2
\<rhd>                  code: 0x0022b3
\<unlhd>                code: 0x0022b4
\<unrhd>                code: 0x0022b5
\<triangleleft>         code: 0x0025c3
\<triangleright>        code: 0x0025b9
\<triangle>             code: 0x0025b3
\<triangleq>            code: 0x00225c
\<oplus>                code: 0x002295  abbrev: +o
\<Oplus>                code: 0x002a01  abbrev: +O
\<otimes>               code: 0x002297  abbrev: *o
\<Otimes>               code: 0x002a02  abbrev: *O
\<odot>                 code: 0x002299  abbrev: .o
\<Odot>                 code: 0x002a00  abbrev: .O
\<ominus>               code: 0x002296  abbrev: -o
\<oslash>               code: 0x002298  abbrev: /o
\<dots>                 code: 0x002026  abbrev: ...
\<cdots>                code: 0x0022ef
\<Sum>                  code: 0x002211  abbrev: SUM
\<Prod>                 code: 0x00220f  abbrev: PROD
\<Coprod>               code: 0x002210
\<infinity>             code: 0x00221e
\<integral>             code: 0x00222b
\<ointegral>            code: 0x00222e
\<clubsuit>             code: 0x002663
\<diamondsuit>          code: 0x002662
\<heartsuit>            code: 0x002661
\<spadesuit>            code: 0x002660
\<aleph>                code: 0x002135
\<emptyset>             code: 0x002205
\<nabla>                code: 0x002207
\<partial>              code: 0x002202
\<Re>                   code: 0x00211c
\<Im>                   code: 0x002111
\<flat>                 code: 0x00266d
\<natural>              code: 0x00266e
\<sharp>                code: 0x00266f
\<angle>                code: 0x002220
\<copyright>            code: 0x0000a9
\<registered>           code: 0x0000ae
\<hyphen>               code: 0x0000ad
\<inverse>              code: 0x0000af
\<onesuperior>          code: 0x0000b9
\<onequarter>           code: 0x0000bc
\<twosuperior>          code: 0x0000b2
\<onehalf>              code: 0x0000bd
\<threesuperior>        code: 0x0000b3
\<threequarters>        code: 0x0000be
\<ordfeminine>          code: 0x0000aa
\<ordmasculine>         code: 0x0000ba
\<section>              code: 0x0000a7
\<paragraph>            code: 0x0000b6
\<exclamdown>           code: 0x0000a1
\<questiondown>         code: 0x0000bf
\<euro>                 code: 0x0020ac
\<pounds>               code: 0x0000a3
\<yen>                  code: 0x0000a5
\<cent>                 code: 0x0000a2
\<currency>             code: 0x0000a4
\<degree>               code: 0x0000b0
\<amalg>                code: 0x002a3f
\<mho>                  code: 0x002127
\<lozenge>              code: 0x0025ca
\<wp>                   code: 0x002118
\<wrong>                code: 0x002240
\<struct>               code: 0x0022c4
\<acute>                code: 0x0000b4
\<index>                code: 0x000131
\<dieresis>             code: 0x0000a8
\<cedilla>              code: 0x0000b8
\<hungarumlaut>         code: 0x0002dd
\<spacespace>           code: 0x002423
\<some>                 code: 0x0003f5
\<^sub>                 code: 0x0021e9  abbrev: =_
\<^sup>                 code: 0x0021e7  abbrev: =^
\<^isub>                code: 0x0021e3  abbrev: -_
\<^isup>                code: 0x0021e1  abbrev: -^
\<^bsub>                code: 0x0021d8  abbrev: =_(
\<^esub>                code: 0x0021d9  abbrev: =_)
\<^bsup>                code: 0x0021d7  abbrev: =^(
\<^esup>                code: 0x0021d6  abbrev: =^)
\<^bold>                code: 0x002759  abbrev: -.