--- 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")];