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>",