diff -r 4d501db6ebed -r b7562e452816 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Tue Apr 29 17:23:53 1997 +0200
+++ b/lib/scripts/symbolinput.pl	Tue Apr 29 17:38:02 1997 +0200
@@ -6,21 +6,6 @@
 
 %tab = (
 #GENERATED TEXT FOLLOWS - Do not edit!
-  "\x91", "\\<lless>",
-  "\x92", "\\<unlhd>",
-  "\x93", "\\<lhd>",
-  "\x94", "\\<rhd>",
-  "\x95", "\\<tturnstile>",
-  "\x96", "\\<langle>",
-  "\x97", "\\<rangle>",
-  "\x98", "\\<orelse>",
-  "\x99", "\\<top>",
-  "\x9a", "\\<Or>",
-  "\x9b", "\\<ocdot>",
-  "\x9c", "\\<iota>",
-  "\x9d", "\\<upsilon>",
-  "\x9e", "\\<Upsilon>",
-  "\x9f", "\\<Xi>",
   "\xa0", "\\<space2>",
   "\xa1", "\\<Gamma>",
   "\xa2", "\\<Delta>",