# HG changeset patch
# User wenzelm
# Date 860951454 -7200
# Node ID ada10e31bf66fef4623e68d10d07471501deb2c2
# Parent  b228efa26ea3d856b069e81873058a1ad397d8f0
GENERATED TEXT;

diff -r b228efa26ea3 -r ada10e31bf66 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Sun Apr 13 19:10:27 1997 +0200
+++ b/src/Pure/Syntax/symbol_font.ML	Sun Apr 13 19:10:54 1997 +0200
@@ -32,6 +32,7 @@
 
 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",
@@ -44,6 +45,7 @@
   "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 *)
 ];
 
 val enc_rel = enc_vector ~~ (map chr (enc_start upto enc_end));