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