src/ZF/Ordinal.ML

 by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
 qed "Ord_contains_Transset";
 
 (*** 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";
 
 (* Ord(succ(j)) ==> Ord(j) *)
 val Ord_succD = succI1 RSN (2, Ord_in_Ord);

 Goal "[| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)";
 by (REPEAT (ares_tac [OrdI] 1
      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";
 
 Goal "[| i:j;  j:k;  Ord(k) |] ==> i:k";
 by (REPEAT (ares_tac [OrdmemD RS subsetD] 1));