# HG changeset patch
# User wenzelm
# Date 857745136 -3600
# Node ID 77903c147673721d9034e0276d0cf7e2ff540741
# Parent  bc6d915b8019165367f2c6137a68889f2c5b6de5
removed lparr, rparr, empty, succeq, ge, rrightarrow;
added turnstile, Turnstile, cdot, approx, Colon, bow;
renamed tick to surd;

diff -r bc6d915b8019 -r 77903c147673 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Fri Mar 07 15:30:23 1997 +0100
+++ b/lib/scripts/symbolinput.pl	Fri Mar 07 15:32:16 1997 +0100
@@ -46,11 +46,11 @@
   "\xc6", "\\\\<rceil>",
   "\xc7", "\\\\<lfloor>",
   "\xc8", "\\\\<rfloor>",
-  "\xc9", "\\\\<lparr>",
-  "\xca", "\\\\<rparr>",
+  "\xc9", "\\\\<turnstile>",
+  "\xca", "\\\\<Turnstile>",
   "\xcb", "\\\\<lbrakk>",
   "\xcc", "\\\\<rbrakk>",
-  "\xcd", "\\\\<empty>",
+  "\xcd", "\\\\<cdot>",
   "\xce", "\\\\<in>",
   "\xcf", "\\\\<subseteq>",
   "\xd0", "\\\\<inter>",
@@ -70,18 +70,18 @@
   "\xde", "\\\\<prec>",
   "\xdf", "\\\\<preceq>",
   "\xe0", "\\\\<succ>",
-  "\xe1", "\\\\<succeq>",
+  "\xe1", "\\\\<approx>",
   "\xe2", "\\\\<sim>",
   "\xe3", "\\\\<simeq>",
   "\xe4", "\\\\<le>",
-  "\xe5", "\\\\<ge>",
+  "\xe5", "\\\\<Colon>",
   "\xe6", "\\\\<leftarrow>",
   "\xe7", "\\\\<midarrow>",
   "\xe8", "\\\\<rightarrow>",
   "\xe9", "\\\\<Leftarrow>",
   "\xea", "\\\\<Midarrow>",
   "\xeb", "\\\\<Rightarrow>",
-  "\xec", "\\\\<rrightarrow>",
+  "\xec", "\\\\<bow>",
   "\xed", "\\\\<mapsto>",
   "\xee", "\\\\<leadsto>",
   "\xef", "\\\\<up>",
@@ -99,7 +99,7 @@
   "\xfb", "\\\\<circ>",
   "\xfc", "\\\\<bullet>",
   "\xfd", "\\\\<parallel>",
-  "\xfe", "\\\\<tick>",
+  "\xfe", "\\\\<surd>",
   "\xff", "\\\\<copyright>");
 
 $SIG{INT} = "IGNORE";
diff -r bc6d915b8019 -r 77903c147673 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Fri Mar 07 15:30:23 1997 +0100
+++ b/src/Pure/Syntax/symbol_font.ML	Fri Mar 07 15:32:16 1997 +0100
@@ -34,13 +34,13 @@
   "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", "lparr", "rparr", "lbrakk", "rbrakk", "empty", "in", "subseteq",
+  "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", "succeq", "sim", "simeq", "le", "ge", "leftarrow", "midarrow",
-  "rightarrow", "Leftarrow", "Midarrow", "Rightarrow", "rrightarrow", "mapsto", "leadsto", "up",
+  "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", "tick", "copyright"
+  "infinity", "box", "diamond", "circ", "bullet", "parallel", "surd", "copyright"
 ];
 
 val enc_rel = enc_vector ~~ (map chr (enc_start upto enc_end));