# HG changeset patch
# User oheimb
# Date 850747502 -3600
# Node ID 4550426cf8f78473331ede5667187a68dac7fb63
# Parent  49a49fc4a0f0fddb0306d352b97e68fea28e943e
added consistency comment

diff -r 49a49fc4a0f0 -r 4550426cf8f7 lib/scripts/symbol_input.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/symbol_input.pl	Mon Dec 16 15:45:02 1996 +0100
@@ -0,0 +1,112 @@
+# Title:	Distribution/lib/scripts/symbol_input.pl
+# ID:		$Id$
+# Author:	Markus Wenzel, David von Oheimb
+# Copyright	1996 Technische Universitaet Muenchen
+#
+# translate symbols into \<...> sequences.
+# table must be consistent with Pure/Syntax/symbol_font.ML
+
+%tab = (
+  "\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", "\\\\<lceil>",
+  "\xc6", "\\\\<rceil>",
+  "\xc7", "\\\\<lfloor>",
+  "\xc8", "\\\\<rfloor>",
+  "\xc9", "\\\\<lparr>",
+  "\xca", "\\\\<rparr>",
+  "\xcb", "\\\\<lbrakk>",
+  "\xcc", "\\\\<rbrakk>",
+  "\xcd", "\\\\<empty>",
+  "\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", "\\\\<succeq>",
+  "\xe2", "\\\\<sim>",
+  "\xe3", "\\\\<simeq>",
+  "\xe4", "\\\\<le>",
+  "\xe5", "\\\\<ge>",
+  "\xe6", "\\\\<leftarrow>",
+  "\xe7", "\\\\<midarrow>",
+  "\xe8", "\\\\<rightarrow>",
+  "\xe9", "\\\\<Leftarrow>",
+  "\xea", "\\\\<Midarrow>",
+  "\xeb", "\\\\<Rightarrow>",
+  "\xec", "\\\\<rrightarrow>",
+  "\xed", "\\\\<mapsto>",
+  "\xee", "\\\\<leadsto>",
+  "\xef", "\\\\<up>",
+  "\xf0", "\\\\<down>",
+  "\xf1", "\\\\<notin>",
+  "\xf2", "\\\\<times>",
+  "\xf3", "\\\\<oplus>",
+  "\xf4", "\\\\<ominus>",
+  "\xf5", "\\\\<otimes>",
+  "\xf6", "\\\\<oslash>",
+  "\xf7", "\\\\<natural>",
+  "\xf8", "\\\\<infinity>",
+  "\xf9", "\\\\<box>",
+  "\xfa", "\\\\<diamond>",
+  "\xfb", "\\\\<circ>",
+  "\xfc", "\\\\<bullet>",
+  "\xfd", "\\\\<parallel>",
+  "\xfe", "\\\\<tick>",
+  "\xff", "\\\\<copyright>");
+
+$SIG{INT} = "IGNORE";
+$| = 1;
+
+while (<ARGV>) {
+  s/([\xa1-\xff])/$tab{$1}/g;
+  print;
+}
diff -r 49a49fc4a0f0 -r 4550426cf8f7 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Mon Dec 16 15:45:01 1996 +0100
+++ b/lib/scripts/symbolinput.pl	Mon Dec 16 15:45:02 1996 +0100
@@ -4,6 +4,7 @@
 # Copyright	1996 Technische Universitaet Muenchen
 #
 # translate symbols into \<...> sequences.
+# table must be consistent with Pure/Syntax/symbol_font.ML
 
 %tab = (
   "\xa1", "\\\\<Gamma>",
diff -r 49a49fc4a0f0 -r 4550426cf8f7 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 15:45:01 1996 +0100
+++ b/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 15:45:02 1996 +0100
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
 
 The Isabelle symbol font.
-enc_vector must be consistent with Distribution/lib/scripts/symbol_input.pl
+enc_vector must be consistent with Distribution/lib/scripts/symbolinput.pl
 *)
 
 signature SYMBOL_FONT =