# HG changeset patch
# User wenzelm
# Date 861209616 -7200
# Node ID 89db5eedecabf2c32f936e0eb28e5a17ef76d552
# Parent  09e87e779b7d3b0ea6b1fbc358ac6cc2f03dd323
removed lceil, rceil, lfloor, rfloor;

diff -r 09e87e779b7d -r 89db5eedecab lib/encodings/isabelle-0
--- 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
diff -r 09e87e779b7d -r 89db5eedecab lib/scripts/symbolinput.pl
--- 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>",
diff -r 09e87e779b7d -r 89db5eedecab src/Pure/Syntax/symbol_font.ML
--- 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",