2943

1 
#


2 
# $Id$

2397

3 
#

2943

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


5 
#

2397

6 


7 
%tab = (

2943

8 
#GENERATED TEXT FOLLOWS  Do not edit!

2945

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>",

2967

45 
"\xc5", "\\<undef197>",


46 
"\xc6", "\\<undef198>",


47 
"\xc7", "\\<undef199>",


48 
"\xc8", "\\<undef200>",

2945

49 
"\xc9", "\\<turnstile>",


50 
"\xca", "\\<Turnstile>",


51 
"\xcb", "\\<lbrakk>",


52 
"\xcc", "\\<rbrakk>",


53 
"\xcd", "\\<cdot>",


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>",


73 
"\xe1", "\\<approx>",


74 
"\xe2", "\\<sim>",


75 
"\xe3", "\\<simeq>",


76 
"\xe4", "\\<le>",


77 
"\xe5", "\\<Colon>",


78 
"\xe6", "\\<leftarrow>",


79 
"\xe7", "\\<midarrow>",


80 
"\xe8", "\\<rightarrow>",


81 
"\xe9", "\\<Leftarrow>",


82 
"\xea", "\\<Midarrow>",


83 
"\xeb", "\\<Rightarrow>",


84 
"\xec", "\\<bow>",


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>",


95 
"\xf7", "\\<subset>",


96 
"\xf8", "\\<infinity>",


97 
"\xf9", "\\<box>",


98 
"\xfa", "\\<diamond>",


99 
"\xfb", "\\<circ>",


100 
"\xfc", "\\<bullet>",


101 
"\xfd", "\\<parallel>",


102 
"\xfe", "\\<surd>",


103 
"\xff", "\\<copyright>"

2943

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 
}
