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!

3064

9 
"\xa0", "\\<space2>",

2945

10 
"\xa1", "\\<Gamma>",


11 
"\xa2", "\\<Delta>",


12 
"\xa3", "\\<Theta>",


13 
"\xa4", "\\<Lambda>",


14 
"\xa5", "\\<Pi>",


15 
"\xa6", "\\<Sigma>",


16 
"\xa7", "\\<Phi>",


17 
"\xa8", "\\<Psi>",


18 
"\xa9", "\\<Omega>",


19 
"\xaa", "\\<alpha>",


20 
"\xab", "\\<beta>",


21 
"\xac", "\\<gamma>",


22 
"\xad", "\\<delta>",


23 
"\xae", "\\<epsilon>",


24 
"\xaf", "\\<zeta>",


25 
"\xb0", "\\<eta>",


26 
"\xb1", "\\<theta>",


27 
"\xb2", "\\<kappa>",


28 
"\xb3", "\\<lambda>",


29 
"\xb4", "\\<mu>",


30 
"\xb5", "\\<nu>",


31 
"\xb6", "\\<xi>",


32 
"\xb7", "\\<pi>",


33 
"\xb8", "\\<rho>",


34 
"\xb9", "\\<sigma>",


35 
"\xba", "\\<tau>",


36 
"\xbb", "\\<phi>",


37 
"\xbc", "\\<chi>",


38 
"\xbd", "\\<psi>",


39 
"\xbe", "\\<omega>",


40 
"\xbf", "\\<not>",


41 
"\xc0", "\\<and>",


42 
"\xc1", "\\<or>",


43 
"\xc2", "\\<forall>",


44 
"\xc3", "\\<exists>",


45 
"\xc4", "\\<And>",

3064

46 
"\xc5", "\\<lceil>",


47 
"\xc6", "\\<rceil>",


48 
"\xc7", "\\<lfloor>",


49 
"\xc8", "\\<rfloor>",

2945

50 
"\xc9", "\\<turnstile>",


51 
"\xca", "\\<Turnstile>",


52 
"\xcb", "\\<lbrakk>",


53 
"\xcc", "\\<rbrakk>",


54 
"\xcd", "\\<cdot>",


55 
"\xce", "\\<in>",


56 
"\xcf", "\\<subseteq>",


57 
"\xd0", "\\<inter>",


58 
"\xd1", "\\<union>",


59 
"\xd2", "\\<Inter>",


60 
"\xd3", "\\<Union>",


61 
"\xd4", "\\<sqinter>",


62 
"\xd5", "\\<squnion>",


63 
"\xd6", "\\<Sqinter>",


64 
"\xd7", "\\<Squnion>",


65 
"\xd8", "\\<bottom>",


66 
"\xd9", "\\<doteq>",


67 
"\xda", "\\<equiv>",


68 
"\xdb", "\\<noteq>",


69 
"\xdc", "\\<sqsubset>",


70 
"\xdd", "\\<sqsubseteq>",


71 
"\xde", "\\<prec>",


72 
"\xdf", "\\<preceq>",


73 
"\xe0", "\\<succ>",


74 
"\xe1", "\\<approx>",


75 
"\xe2", "\\<sim>",


76 
"\xe3", "\\<simeq>",


77 
"\xe4", "\\<le>",


78 
"\xe5", "\\<Colon>",


79 
"\xe6", "\\<leftarrow>",


80 
"\xe7", "\\<midarrow>",


81 
"\xe8", "\\<rightarrow>",


82 
"\xe9", "\\<Leftarrow>",


83 
"\xea", "\\<Midarrow>",


84 
"\xeb", "\\<Rightarrow>",


85 
"\xec", "\\<bow>",


86 
"\xed", "\\<mapsto>",


87 
"\xee", "\\<leadsto>",


88 
"\xef", "\\<up>",


89 
"\xf0", "\\<down>",


90 
"\xf1", "\\<notin>",


91 
"\xf2", "\\<times>",


92 
"\xf3", "\\<oplus>",


93 
"\xf4", "\\<ominus>",


94 
"\xf5", "\\<otimes>",


95 
"\xf6", "\\<oslash>",


96 
"\xf7", "\\<subset>",


97 
"\xf8", "\\<infinity>",


98 
"\xf9", "\\<box>",


99 
"\xfa", "\\<diamond>",


100 
"\xfb", "\\<circ>",


101 
"\xfc", "\\<bullet>",


102 
"\xfd", "\\<parallel>",


103 
"\xfe", "\\<surd>",


104 
"\xff", "\\<copyright>"

2943

105 
#END OF GENERATED TEXT


106 
);

2397

107 


108 
$SIG{INT} = "IGNORE";


109 
$ = 1;


110 


111 
while (<ARGV>) {

2943

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

2397

113 
print;


114 
}
