--- a/src/ZF/Ordinal.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Ordinal.ML Wed Jul 15 10:15:13 1998 +0200
@@ -103,7 +103,7 @@
(*** Lemmas for ordinals ***)
-Goalw [Ord_def,Transset_def] "!!i j.[| Ord(i); j:i |] ==> Ord(j)";
+Goalw [Ord_def,Transset_def] "[| Ord(i); j:i |] ==> Ord(j)";
by (Blast_tac 1);
qed "Ord_in_Ord";
@@ -117,7 +117,7 @@
ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
qed "Ord_subset_Ord";
-Goalw [Ord_def,Transset_def] "!!i j. [| j:i; Ord(i) |] ==> j<=i";
+Goalw [Ord_def,Transset_def] "[| j:i; Ord(i) |] ==> j<=i";
by (Blast_tac 1);
qed "OrdmemD";