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