author | wenzelm |
Sun, 13 Apr 1997 19:11:32 +0200 | |
changeset 2943 | 04a66be5e790 |
parent 2769 | 77903c147673 |
child 2945 | b4f3840a42f8 |
permissions | -rw-r--r-- |
2943 | 1 |
# |
2 |
# $Id$ |
|
2397 | 3 |
# |
2943 | 4 |
# symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences. |
5 |
# |
|
2397 | 6 |
|
7 |
%tab = ( |
|
2943 | 8 |
#GENERATED TEXT FOLLOWS - Do not edit! |
2397 | 9 |
"\xa1", "\\\\<Gamma>", |
10 |
"\xa2", "\\\\<Delta>", |
|
11 |
"\xa3", "\\\\<Theta>", |
|
12 |
"\xa4", "\\\\<Lambda>", |
|
13 |
"\xa5", "\\\\<Pi>", |
|
14 |
"\xa6", "\\\\<Sigma>", |
|
15 |
"\xa7", "\\\\<Phi>", |
|
16 |
"\xa8", "\\\\<Psi>", |
|
17 |
"\xa9", "\\\\<Omega>", |
|
18 |
"\xaa", "\\\\<alpha>", |
|
19 |
"\xab", "\\\\<beta>", |
|
20 |
"\xac", "\\\\<gamma>", |
|
21 |
"\xad", "\\\\<delta>", |
|
22 |
"\xae", "\\\\<epsilon>", |
|
23 |
"\xaf", "\\\\<zeta>", |
|
24 |
"\xb0", "\\\\<eta>", |
|
25 |
"\xb1", "\\\\<theta>", |
|
26 |
"\xb2", "\\\\<kappa>", |
|
27 |
"\xb3", "\\\\<lambda>", |
|
28 |
"\xb4", "\\\\<mu>", |
|
29 |
"\xb5", "\\\\<nu>", |
|
30 |
"\xb6", "\\\\<xi>", |
|
31 |
"\xb7", "\\\\<pi>", |
|
32 |
"\xb8", "\\\\<rho>", |
|
33 |
"\xb9", "\\\\<sigma>", |
|
34 |
"\xba", "\\\\<tau>", |
|
35 |
"\xbb", "\\\\<phi>", |
|
36 |
"\xbc", "\\\\<chi>", |
|
37 |
"\xbd", "\\\\<psi>", |
|
38 |
"\xbe", "\\\\<omega>", |
|
39 |
"\xbf", "\\\\<not>", |
|
40 |
"\xc0", "\\\\<and>", |
|
41 |
"\xc1", "\\\\<or>", |
|
42 |
"\xc2", "\\\\<forall>", |
|
43 |
"\xc3", "\\\\<exists>", |
|
44 |
"\xc4", "\\\\<And>", |
|
45 |
"\xc5", "\\\\<lceil>", |
|
46 |
"\xc6", "\\\\<rceil>", |
|
47 |
"\xc7", "\\\\<lfloor>", |
|
48 |
"\xc8", "\\\\<rfloor>", |
|
2769
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
49 |
"\xc9", "\\\\<turnstile>", |
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
50 |
"\xca", "\\\\<Turnstile>", |
2397 | 51 |
"\xcb", "\\\\<lbrakk>", |
52 |
"\xcc", "\\\\<rbrakk>", |
|
2769
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
53 |
"\xcd", "\\\\<cdot>", |
2397 | 54 |
"\xce", "\\\\<in>", |
55 |
"\xcf", "\\\\<subseteq>", |
|
56 |
"\xd0", "\\\\<inter>", |
|
57 |
"\xd1", "\\\\<union>", |
|
58 |
"\xd2", "\\\\<Inter>", |
|
59 |
"\xd3", "\\\\<Union>", |
|
60 |
"\xd4", "\\\\<sqinter>", |
|
61 |
"\xd5", "\\\\<squnion>", |
|
62 |
"\xd6", "\\\\<Sqinter>", |
|
63 |
"\xd7", "\\\\<Squnion>", |
|
64 |
"\xd8", "\\\\<bottom>", |
|
65 |
"\xd9", "\\\\<doteq>", |
|
66 |
"\xda", "\\\\<equiv>", |
|
67 |
"\xdb", "\\\\<noteq>", |
|
68 |
"\xdc", "\\\\<sqsubset>", |
|
69 |
"\xdd", "\\\\<sqsubseteq>", |
|
70 |
"\xde", "\\\\<prec>", |
|
71 |
"\xdf", "\\\\<preceq>", |
|
72 |
"\xe0", "\\\\<succ>", |
|
2769
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
73 |
"\xe1", "\\\\<approx>", |
2397 | 74 |
"\xe2", "\\\\<sim>", |
75 |
"\xe3", "\\\\<simeq>", |
|
76 |
"\xe4", "\\\\<le>", |
|
2769
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
77 |
"\xe5", "\\\\<Colon>", |
2397 | 78 |
"\xe6", "\\\\<leftarrow>", |
79 |
"\xe7", "\\\\<midarrow>", |
|
80 |
"\xe8", "\\\\<rightarrow>", |
|
81 |
"\xe9", "\\\\<Leftarrow>", |
|
82 |
"\xea", "\\\\<Midarrow>", |
|
83 |
"\xeb", "\\\\<Rightarrow>", |
|
2769
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
84 |
"\xec", "\\\\<bow>", |
2397 | 85 |
"\xed", "\\\\<mapsto>", |
86 |
"\xee", "\\\\<leadsto>", |
|
87 |
"\xef", "\\\\<up>", |
|
88 |
"\xf0", "\\\\<down>", |
|
89 |
"\xf1", "\\\\<notin>", |
|
90 |
"\xf2", "\\\\<times>", |
|
91 |
"\xf3", "\\\\<oplus>", |
|
92 |
"\xf4", "\\\\<ominus>", |
|
93 |
"\xf5", "\\\\<otimes>", |
|
94 |
"\xf6", "\\\\<oslash>", |
|
2676 | 95 |
"\xf7", "\\\\<subset>", |
2397 | 96 |
"\xf8", "\\\\<infinity>", |
97 |
"\xf9", "\\\\<box>", |
|
98 |
"\xfa", "\\\\<diamond>", |
|
99 |
"\xfb", "\\\\<circ>", |
|
100 |
"\xfc", "\\\\<bullet>", |
|
101 |
"\xfd", "\\\\<parallel>", |
|
2769
77903c147673
removed lparr, rparr, empty, succeq, ge, rrightarrow;
wenzelm
parents:
2676
diff
changeset
|
102 |
"\xfe", "\\\\<surd>", |
2943 | 103 |
"\xff", "\\\\<copyright>" |
104 |
#END OF GENERATED TEXT |
|
105 |
); |
|
2397 | 106 |
|
107 |
$SIG{INT} = "IGNORE"; |
|
108 |
$| = 1; |
|
109 |
||
110 |
while (<ARGV>) { |
|
2943 | 111 |
s/([\xa1-\xff])/\\$tab{$1}/g; |
2397 | 112 |
print; |
113 |
} |