removed lceil, rceil, lfloor, rfloor;
authorwenzelm
Wed, 16 Apr 1997 18:53:36 +0200
changeset 2967 89db5eedecab
parent 2966 09e87e779b7d
child 2968 8ba30b031f31
removed lceil, rceil, lfloor, rfloor;
lib/encodings/isabelle-0
lib/scripts/symbolinput.pl
src/Pure/Syntax/symbol_font.ML
--- a/lib/encodings/isabelle-0	Wed Apr 16 18:51:03 1997 +0200
+++ b/lib/encodings/isabelle-0	Wed Apr 16 18:53:36 1997 +0200
@@ -41,10 +41,13 @@
 forall
 exists
 And
-lceil
-rceil
-lfloor
-rfloor
+
+#lceil
+#rceil
+#lfloor
+#rfloor
+
+201:
 turnstile
 Turnstile
 lbrakk
--- a/lib/scripts/symbolinput.pl	Wed Apr 16 18:51:03 1997 +0200
+++ b/lib/scripts/symbolinput.pl	Wed Apr 16 18:53:36 1997 +0200
@@ -42,10 +42,10 @@
   "\xc2", "\\<forall>",
   "\xc3", "\\<exists>",
   "\xc4", "\\<And>",
-  "\xc5", "\\<lceil>",
-  "\xc6", "\\<rceil>",
-  "\xc7", "\\<lfloor>",
-  "\xc8", "\\<rfloor>",
+  "\xc5", "\\<undef197>",
+  "\xc6", "\\<undef198>",
+  "\xc7", "\\<undef199>",
+  "\xc8", "\\<undef200>",
   "\xc9", "\\<turnstile>",
   "\xca", "\\<Turnstile>",
   "\xcb", "\\<lbrakk>",
--- a/src/Pure/Syntax/symbol_font.ML	Wed Apr 16 18:51:03 1997 +0200
+++ b/src/Pure/Syntax/symbol_font.ML	Wed Apr 16 18:53:36 1997 +0200
@@ -68,10 +68,10 @@
   "forall",
   "exists",
   "And",
-  "lceil",
-  "rceil",
-  "lfloor",
-  "rfloor",
+  "undef197",
+  "undef198",
+  "undef199",
+  "undef200",
   "turnstile",
   "Turnstile",
   "lbrakk",