#
# $Id$
#
# symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences.
#
%tab = (
#GENERATED TEXT FOLLOWS - Do not edit!
"\xa1", "\\<Gamma>",
"\xa2", "\\<Delta>",
"\xa3", "\\<Theta>",
"\xa4", "\\<Lambda>",
"\xa5", "\\<Pi>",
"\xa6", "\\<Sigma>",
"\xa7", "\\<Phi>",
"\xa8", "\\<Psi>",
"\xa9", "\\<Omega>",
"\xaa", "\\<alpha>",
"\xab", "\\<beta>",
"\xac", "\\<gamma>",
"\xad", "\\<delta>",
"\xae", "\\<epsilon>",
"\xaf", "\\<zeta>",
"\xb0", "\\<eta>",
"\xb1", "\\<theta>",
"\xb2", "\\<kappa>",
"\xb3", "\\<lambda>",
"\xb4", "\\<mu>",
"\xb5", "\\<nu>",
"\xb6", "\\<xi>",
"\xb7", "\\<pi>",
"\xb8", "\\<rho>",
"\xb9", "\\<sigma>",
"\xba", "\\<tau>",
"\xbb", "\\<phi>",
"\xbc", "\\<chi>",
"\xbd", "\\<psi>",
"\xbe", "\\<omega>",
"\xbf", "\\<not>",
"\xc0", "\\<and>",
"\xc1", "\\<or>",
"\xc2", "\\<forall>",
"\xc3", "\\<exists>",
"\xc4", "\\<And>",
"\xc5", "\\<undef197>",
"\xc6", "\\<undef198>",
"\xc7", "\\<undef199>",
"\xc8", "\\<undef200>",
"\xc9", "\\<turnstile>",
"\xca", "\\<Turnstile>",
"\xcb", "\\<lbrakk>",
"\xcc", "\\<rbrakk>",
"\xcd", "\\<cdot>",
"\xce", "\\<in>",
"\xcf", "\\<subseteq>",
"\xd0", "\\<inter>",
"\xd1", "\\<union>",
"\xd2", "\\<Inter>",
"\xd3", "\\<Union>",
"\xd4", "\\<sqinter>",
"\xd5", "\\<squnion>",
"\xd6", "\\<Sqinter>",
"\xd7", "\\<Squnion>",
"\xd8", "\\<bottom>",
"\xd9", "\\<doteq>",
"\xda", "\\<equiv>",
"\xdb", "\\<noteq>",
"\xdc", "\\<sqsubset>",
"\xdd", "\\<sqsubseteq>",
"\xde", "\\<prec>",
"\xdf", "\\<preceq>",
"\xe0", "\\<succ>",
"\xe1", "\\<approx>",
"\xe2", "\\<sim>",
"\xe3", "\\<simeq>",
"\xe4", "\\<le>",
"\xe5", "\\<Colon>",
"\xe6", "\\<leftarrow>",
"\xe7", "\\<midarrow>",
"\xe8", "\\<rightarrow>",
"\xe9", "\\<Leftarrow>",
"\xea", "\\<Midarrow>",
"\xeb", "\\<Rightarrow>",
"\xec", "\\<bow>",
"\xed", "\\<mapsto>",
"\xee", "\\<leadsto>",
"\xef", "\\<up>",
"\xf0", "\\<down>",
"\xf1", "\\<notin>",
"\xf2", "\\<times>",
"\xf3", "\\<oplus>",
"\xf4", "\\<ominus>",
"\xf5", "\\<otimes>",
"\xf6", "\\<oslash>",
"\xf7", "\\<subset>",
"\xf8", "\\<infinity>",
"\xf9", "\\<box>",
"\xfa", "\\<diamond>",
"\xfb", "\\<circ>",
"\xfc", "\\<bullet>",
"\xfd", "\\<parallel>",
"\xfe", "\\<surd>",
"\xff", "\\<copyright>"
#END OF GENERATED TEXT
);
$SIG{INT} = "IGNORE";
$| = 1;
while (<ARGV>) {
s/([\xa1-\xff])/\\$tab{$1}/g;
print;
}