author | wenzelm |
Fri, 12 Oct 2001 12:05:46 +0200 | |
changeset 11724 | f727aa96ae2e |
parent 9960 | 07521b6eb888 |
permissions | -rw-r--r-- |
2864 | 1 |
# |
2 |
# $Id$ |
|
9818 | 3 |
# Author: Markus Wenzel, TU Muenchen |
4 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
2864 | 5 |
# |
6 |
# The isabelle-0 encoding table. |
|
7 |
# |
|
8 |
||
3068
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
9 |
#145: |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
10 |
# |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
11 |
#lless |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
12 |
#unlhd |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
13 |
#lhd |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
14 |
#rhd |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
15 |
#tturnstile |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
16 |
#langle |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
17 |
#rangle |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
18 |
#orelse |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
19 |
#top |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
20 |
#Or |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
21 |
#ocdot |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
22 |
#iota |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
23 |
#upsilon |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
24 |
#Upsilon |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
25 |
#Xi |
3064 | 26 |
|
3068
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
27 |
160: |
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3067
diff
changeset
|
28 |
|
6281 | 29 |
spacespace |
2864 | 30 |
Gamma |
31 |
Delta |
|
32 |
Theta |
|
33 |
Lambda |
|
34 |
Pi |
|
35 |
Sigma |
|
36 |
Phi |
|
37 |
Psi |
|
38 |
Omega |
|
39 |
alpha |
|
40 |
beta |
|
41 |
gamma |
|
42 |
delta |
|
43 |
epsilon |
|
44 |
zeta |
|
45 |
eta |
|
46 |
theta |
|
47 |
kappa |
|
48 |
lambda |
|
49 |
mu |
|
50 |
nu |
|
51 |
xi |
|
52 |
pi |
|
53 |
rho |
|
54 |
sigma |
|
55 |
tau |
|
56 |
phi |
|
57 |
chi |
|
58 |
psi |
|
59 |
omega |
|
60 |
not |
|
61 |
and |
|
62 |
or |
|
63 |
forall |
|
64 |
exists |
|
65 |
And |
|
3064 | 66 |
lceil |
67 |
rceil |
|
68 |
lfloor |
|
69 |
rfloor |
|
2864 | 70 |
turnstile |
71 |
Turnstile |
|
72 |
lbrakk |
|
73 |
rbrakk |
|
74 |
cdot |
|
75 |
in |
|
76 |
subseteq |
|
77 |
inter |
|
78 |
union |
|
79 |
Inter |
|
80 |
Union |
|
81 |
sqinter |
|
82 |
squnion |
|
83 |
Sqinter |
|
84 |
Squnion |
|
85 |
bottom |
|
86 |
doteq |
|
87 |
equiv |
|
88 |
noteq |
|
89 |
sqsubset |
|
90 |
sqsubseteq |
|
91 |
prec |
|
92 |
preceq |
|
93 |
succ |
|
94 |
approx |
|
95 |
sim |
|
96 |
simeq |
|
97 |
le |
|
98 |
Colon |
|
99 |
leftarrow |
|
100 |
midarrow |
|
101 |
rightarrow |
|
102 |
Leftarrow |
|
103 |
Midarrow |
|
104 |
Rightarrow |
|
9960 | 105 |
frown |
2864 | 106 |
mapsto |
107 |
leadsto |
|
108 |
up |
|
109 |
down |
|
110 |
notin |
|
111 |
times |
|
112 |
oplus |
|
113 |
ominus |
|
114 |
otimes |
|
115 |
oslash |
|
116 |
subset |
|
117 |
infinity |
|
118 |
box |
|
119 |
diamond |
|
120 |
circ |
|
121 |
bullet |
|
122 |
parallel |
|
123 |
surd |
|
124 |
copyright |