src/ZF/Ordinal.ML

 qed "Transset_iff_Union_succ";
 
 (** Consequences of downwards closure **)
 
 Goalw [Transset_def]
-    "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
+    "[| Transset(C); {a,b}: C |] ==> a:C & b: C";
 by (Blast_tac 1);
 qed "Transset_doubleton_D";
 
 val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
     "[| Transset(C); <a,b>: C |] ==> a:C & b: C";

 Goalw [Transset_def] "Transset(0)";
 by (Blast_tac 1);
 qed "Transset_0";
 
 Goalw [Transset_def]
-    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Un j)";
+    "[| Transset(i);  Transset(j) |] ==> Transset(i Un j)";
 by (Blast_tac 1);
 qed "Transset_Un";
 
 Goalw [Transset_def]
-    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Int j)";
+    "[| Transset(i);  Transset(j) |] ==> Transset(i Int j)";
 by (Blast_tac 1);
 qed "Transset_Int";
 
 Goalw [Transset_def] "Transset(i) ==> Transset(succ(i))";
 by (Blast_tac 1);

             REPEAT o assume_tac]);
 qed "wf_Memrel";
 
 (*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
 Goalw [Ord_def, Transset_def, trans_def]
-    "!!i. Ord(i) ==> trans(Memrel(i))";
+    "Ord(i) ==> trans(Memrel(i))";
 by (Blast_tac 1);
 qed "trans_Memrel";
 
 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
 Goalw [Transset_def]
-    "!!A. Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A";
+    "Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A";
 by (Blast_tac 1);
 qed "Transset_Memrel_iff";
 
 
 (*** Transfinite induction ***)

 Goalw [Limit_def] "[| Limit(i);  j<i |] ==> succ(j) < i";
 by (Blast_tac 1);
 qed "Limit_has_succ";
 
 Goalw [Limit_def]
-    "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
+    "[| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
 by (safe_tac subset_cs);
 by (rtac (not_le_iff_lt RS iffD1) 2);
 by (blast_tac le_cs 4);
 by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
 qed "non_succ_LimitI";