1.1 --- a/src/Pure/Syntax/symbol_font.ML	Sun Apr 13 19:10:27 1997 +0200
     1.2 +++ b/src/Pure/Syntax/symbol_font.ML	Sun Apr 13 19:10:54 1997 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4  
     1.5  val enc_vector =
     1.6  [
     1.7 +(* GENERATED TEXT FOLLOWS - Do not edit! *)
     1.8        "Gamma", "Delta", "Theta", "Lambda", "Pi", "Sigma", "Phi",
     1.9    "Psi", "Omega", "alpha", "beta", "gamma", "delta", "epsilon", "zeta",
    1.10    "eta", "theta", "kappa", "lambda", "mu", "nu", "xi", "pi",
    1.11 @@ -44,6 +45,7 @@
    1.12    "rightarrow", "Leftarrow", "Midarrow", "Rightarrow", "bow", "mapsto", "leadsto", "up",
    1.13    "down", "notin", "times", "oplus", "ominus", "otimes", "oslash", "subset",
    1.14    "infinity", "box", "diamond", "circ", "bullet", "parallel", "surd", "copyright"
    1.15 +(* END OF GENERATED TEXT *)
    1.16  ];
    1.17  
    1.18  val enc_rel = enc_vector ~~ (map chr (enc_start upto enc_end));