changeset 3068 | b7562e452816 |
parent 3067 | 4d501db6ebed |
child 3069 | de1f64558c01 |
--- a/src/Pure/Syntax/symbol_font.ML Tue Apr 29 17:23:53 1997 +0200 +++ b/src/Pure/Syntax/symbol_font.ML Tue Apr 29 17:38:02 1997 +0200 @@ -26,27 +26,12 @@ (* tables *) -val enc_start = 145; +val enc_start = 161; val enc_end = 255; val enc_vector = [ (* GENERATED TEXT FOLLOWS - Do not edit! *) - "lless", - "unlhd", - "lhd", - "rhd", - "tturnstile", - "langle", - "rangle", - "orelse", - "top", - "Or", - "ocdot", - "iota", - "upsilon", - "Upsilon", - "Xi", "space2", "Gamma", "Delta",