diff -r 4448d76f87ef -r ff6d7206dd04 hol.thy
--- a/hol.thy	Thu Oct 07 10:29:23 1993 +0100
+++ b/hol.thy	Fri Oct 08 13:46:13 1993 +0100
@@ -46,7 +46,6 @@
 
   (* Alternative Quantifiers *)
 
-  "*The"        :: "[idts, bool] => 'a"               ("(3THE _./ _)" 10)
   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
   "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
   "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
@@ -67,7 +66,6 @@
 
 
 translations
-  "THE xs. P"   => "@ xs. P"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
@@ -133,5 +131,5 @@
 
 
 val print_ast_translation =
-  map alt_ast_tr' [("@", "*The"), ("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
+  map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];