2943

1 
#


2 
# $Id$

9789

3 
# Author: Markus Wenzel, TU Muenchen


4 
# License: GPL (GNU GENERAL PUBLIC LICENSE)

2397

5 
#

2943

6 
# symbolinput.pl  expand isabelle0 encoded chars to \<...> sequences.


7 
#

2397

8 


9 
%tab = (

2943

10 
#GENERATED TEXT FOLLOWS  Do not edit!

6281

11 
"\xa0", "\\<spacespace>",

2945

12 
"\xa1", "\\<Gamma>",


13 
"\xa2", "\\<Delta>",


14 
"\xa3", "\\<Theta>",


15 
"\xa4", "\\<Lambda>",


16 
"\xa5", "\\<Pi>",


17 
"\xa6", "\\<Sigma>",


18 
"\xa7", "\\<Phi>",


19 
"\xa8", "\\<Psi>",


20 
"\xa9", "\\<Omega>",


21 
"\xaa", "\\<alpha>",


22 
"\xab", "\\<beta>",


23 
"\xac", "\\<gamma>",


24 
"\xad", "\\<delta>",


25 
"\xae", "\\<epsilon>",


26 
"\xaf", "\\<zeta>",


27 
"\xb0", "\\<eta>",


28 
"\xb1", "\\<theta>",


29 
"\xb2", "\\<kappa>",


30 
"\xb3", "\\<lambda>",


31 
"\xb4", "\\<mu>",


32 
"\xb5", "\\<nu>",


33 
"\xb6", "\\<xi>",


34 
"\xb7", "\\<pi>",


35 
"\xb8", "\\<rho>",


36 
"\xb9", "\\<sigma>",


37 
"\xba", "\\<tau>",


38 
"\xbb", "\\<phi>",


39 
"\xbc", "\\<chi>",


40 
"\xbd", "\\<psi>",


41 
"\xbe", "\\<omega>",


42 
"\xbf", "\\<not>",


43 
"\xc0", "\\<and>",


44 
"\xc1", "\\<or>",


45 
"\xc2", "\\<forall>",


46 
"\xc3", "\\<exists>",


47 
"\xc4", "\\<And>",

3064

48 
"\xc5", "\\<lceil>",


49 
"\xc6", "\\<rceil>",


50 
"\xc7", "\\<lfloor>",


51 
"\xc8", "\\<rfloor>",

2945

52 
"\xc9", "\\<turnstile>",


53 
"\xca", "\\<Turnstile>",


54 
"\xcb", "\\<lbrakk>",


55 
"\xcc", "\\<rbrakk>",


56 
"\xcd", "\\<cdot>",


57 
"\xce", "\\<in>",


58 
"\xcf", "\\<subseteq>",


59 
"\xd0", "\\<inter>",


60 
"\xd1", "\\<union>",


61 
"\xd2", "\\<Inter>",


62 
"\xd3", "\\<Union>",


63 
"\xd4", "\\<sqinter>",


64 
"\xd5", "\\<squnion>",


65 
"\xd6", "\\<Sqinter>",


66 
"\xd7", "\\<Squnion>",


67 
"\xd8", "\\<bottom>",


68 
"\xd9", "\\<doteq>",


69 
"\xda", "\\<equiv>",


70 
"\xdb", "\\<noteq>",


71 
"\xdc", "\\<sqsubset>",


72 
"\xdd", "\\<sqsubseteq>",


73 
"\xde", "\\<prec>",


74 
"\xdf", "\\<preceq>",


75 
"\xe0", "\\<succ>",


76 
"\xe1", "\\<approx>",


77 
"\xe2", "\\<sim>",


78 
"\xe3", "\\<simeq>",


79 
"\xe4", "\\<le>",


80 
"\xe5", "\\<Colon>",


81 
"\xe6", "\\<leftarrow>",


82 
"\xe7", "\\<midarrow>",


83 
"\xe8", "\\<rightarrow>",


84 
"\xe9", "\\<Leftarrow>",


85 
"\xea", "\\<Midarrow>",


86 
"\xeb", "\\<Rightarrow>",

9961

87 
"\xec", "\\<frown>",

2945

88 
"\xed", "\\<mapsto>",


89 
"\xee", "\\<leadsto>",


90 
"\xef", "\\<up>",


91 
"\xf0", "\\<down>",


92 
"\xf1", "\\<notin>",


93 
"\xf2", "\\<times>",


94 
"\xf3", "\\<oplus>",


95 
"\xf4", "\\<ominus>",


96 
"\xf5", "\\<otimes>",


97 
"\xf6", "\\<oslash>",


98 
"\xf7", "\\<subset>",


99 
"\xf8", "\\<infinity>",


100 
"\xf9", "\\<box>",


101 
"\xfa", "\\<diamond>",


102 
"\xfb", "\\<circ>",


103 
"\xfc", "\\<bullet>",


104 
"\xfd", "\\<parallel>",


105 
"\xfe", "\\<surd>",


106 
"\xff", "\\<copyright>"

2943

107 
#END OF GENERATED TEXT


108 
);

2397

109 


110 
$SIG{INT} = "IGNORE";


111 
$ = 1;


112 


113 
while (<ARGV>) {

2943

114 
s/([\xa1\xff])/\\$tab{$1}/g;

2397

115 
print;


116 
}
