updated;
authorwenzelm
Fri, 15 Sep 2000 00:16:36 +0200
changeset 9961 5a9626118941
parent 9960 07521b6eb888
child 9962 765208b5dd23
updated;
lib/scripts/feeder.pl
lib/scripts/symbolinput.pl
src/Pure/General/symbol.ML
--- a/lib/scripts/feeder.pl	Fri Sep 15 00:16:08 2000 +0200
+++ b/lib/scripts/feeder.pl	Fri Sep 15 00:16:36 2000 +0200
@@ -91,7 +91,7 @@
   "\xe9", "\\<Leftarrow>",
   "\xea", "\\<Midarrow>",
   "\xeb", "\\<Rightarrow>",
-  "\xec", "\\<bow>",
+  "\xec", "\\<frown>",
   "\xed", "\\<mapsto>",
   "\xee", "\\<leadsto>",
   "\xef", "\\<up>",
--- a/lib/scripts/symbolinput.pl	Fri Sep 15 00:16:08 2000 +0200
+++ b/lib/scripts/symbolinput.pl	Fri Sep 15 00:16:36 2000 +0200
@@ -84,7 +84,7 @@
   "\xe9", "\\<Leftarrow>",
   "\xea", "\\<Midarrow>",
   "\xeb", "\\<Rightarrow>",
-  "\xec", "\\<bow>",
+  "\xec", "\\<frown>",
   "\xed", "\\<mapsto>",
   "\xee", "\\<leadsto>",
   "\xef", "\\<up>",
--- a/src/Pure/General/symbol.ML	Fri Sep 15 00:16:08 2000 +0200
+++ b/src/Pure/General/symbol.ML	Fri Sep 15 00:16:36 2000 +0200
@@ -202,7 +202,7 @@
   "\\<Leftarrow>",
   "\\<Midarrow>",
   "\\<Rightarrow>",
-  "\\<bow>",
+  "\\<frown>",
   "\\<mapsto>",
   "\\<leadsto>",
   "\\<up>",