# HG changeset patch
# User wenzelm
# Date 860951492 -7200
# Node ID 04a66be5e790e956d1c96c3d4fe38b99428bba19
# Parent  ada10e31bf66fef4623e68d10d07471501deb2c2
GENERATED TEXT;

diff -r ada10e31bf66 -r 04a66be5e790 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Sun Apr 13 19:10:54 1997 +0200
+++ b/lib/scripts/symbolinput.pl	Sun Apr 13 19:11:32 1997 +0200
@@ -1,11 +1,11 @@
-# Title:	lib/scripts/symbolinput.pl
-# ID:		$Id$
-# Author:	Markus Wenzel and David von Oheimb, TU Muenchen
+#
+# $Id$
 #
-# Translate symbols into \<...> sequences.  Please keep consistent
-# with Pure/Syntax/symbol_font.ML!
+# symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences.
+#
 
 %tab = (
+#GENERATED TEXT FOLLOWS - Do not edit!
   "\xa1", "\\\\<Gamma>",
   "\xa2", "\\\\<Delta>",
   "\xa3", "\\\\<Theta>",
@@ -100,12 +100,14 @@
   "\xfc", "\\\\<bullet>",
   "\xfd", "\\\\<parallel>",
   "\xfe", "\\\\<surd>",
-  "\xff", "\\\\<copyright>");
+  "\xff", "\\\\<copyright>"
+#END OF GENERATED TEXT
+);
 
 $SIG{INT} = "IGNORE";
 $| = 1;
 
 while (<ARGV>) {
-  s/([\xa1-\xff])/$tab{$1}/g;
+  s/([\xa1-\xff])/\\$tab{$1}/g;
   print;
 }
diff -r ada10e31bf66 -r 04a66be5e790 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Sun Apr 13 19:10:54 1997 +0200
+++ b/src/Pure/Syntax/symbol_font.ML	Sun Apr 13 19:11:32 1997 +0200
@@ -2,8 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-The Isabelle symbol font.  Please keep enc_vector consistent with
-lib/scripts/symbolinput.pl!
+The Isabelle symbol font.
 *)
 
 signature SYMBOL_FONT =
@@ -33,18 +32,101 @@
 val enc_vector =
 [
 (* GENERATED TEXT FOLLOWS - Do not edit! *)
-      "Gamma", "Delta", "Theta", "Lambda", "Pi", "Sigma", "Phi",
-  "Psi", "Omega", "alpha", "beta", "gamma", "delta", "epsilon", "zeta",
-  "eta", "theta", "kappa", "lambda", "mu", "nu", "xi", "pi",
-  "rho", "sigma", "tau", "phi", "chi", "psi", "omega", "not",
-  "and", "or", "forall", "exists", "And", "lceil", "rceil", "lfloor",
-  "rfloor", "turnstile", "Turnstile", "lbrakk", "rbrakk", "cdot", "in", "subseteq",
-  "inter", "union", "Inter", "Union", "sqinter", "squnion", "Sqinter", "Squnion",
-  "bottom", "doteq", "equiv", "noteq", "sqsubset", "sqsubseteq", "prec", "preceq",
-  "succ", "approx", "sim", "simeq", "le", "Colon", "leftarrow", "midarrow",
-  "rightarrow", "Leftarrow", "Midarrow", "Rightarrow", "bow", "mapsto", "leadsto", "up",
-  "down", "notin", "times", "oplus", "ominus", "otimes", "oslash", "subset",
-  "infinity", "box", "diamond", "circ", "bullet", "parallel", "surd", "copyright"
+  "Gamma",
+  "Delta",
+  "Theta",
+  "Lambda",
+  "Pi",
+  "Sigma",
+  "Phi",
+  "Psi",
+  "Omega",
+  "alpha",
+  "beta",
+  "gamma",
+  "delta",
+  "epsilon",
+  "zeta",
+  "eta",
+  "theta",
+  "kappa",
+  "lambda",
+  "mu",
+  "nu",
+  "xi",
+  "pi",
+  "rho",
+  "sigma",
+  "tau",
+  "phi",
+  "chi",
+  "psi",
+  "omega",
+  "not",
+  "and",
+  "or",
+  "forall",
+  "exists",
+  "And",
+  "lceil",
+  "rceil",
+  "lfloor",
+  "rfloor",
+  "turnstile",
+  "Turnstile",
+  "lbrakk",
+  "rbrakk",
+  "cdot",
+  "in",
+  "subseteq",
+  "inter",
+  "union",
+  "Inter",
+  "Union",
+  "sqinter",
+  "squnion",
+  "Sqinter",
+  "Squnion",
+  "bottom",
+  "doteq",
+  "equiv",
+  "noteq",
+  "sqsubset",
+  "sqsubseteq",
+  "prec",
+  "preceq",
+  "succ",
+  "approx",
+  "sim",
+  "simeq",
+  "le",
+  "Colon",
+  "leftarrow",
+  "midarrow",
+  "rightarrow",
+  "Leftarrow",
+  "Midarrow",
+  "Rightarrow",
+  "bow",
+  "mapsto",
+  "leadsto",
+  "up",
+  "down",
+  "notin",
+  "times",
+  "oplus",
+  "ominus",
+  "otimes",
+  "oslash",
+  "subset",
+  "infinity",
+  "box",
+  "diamond",
+  "circ",
+  "bullet",
+  "parallel",
+  "surd",
+  "copyright"
 (* END OF GENERATED TEXT *)
 ];