1.1 --- a/src/ZF/Ordinal.ML	Sat Dec 22 19:42:35 2001 +0100
     1.2 +++ b/src/ZF/Ordinal.ML	Sat Dec 22 19:46:16 2001 +0100
     1.3 @@ -691,9 +691,15 @@
     1.4  by (assume_tac 1);
     1.5  by (etac (Limit_is_Ord RS Ord_succD RS le_refl) 1);
     1.6  qed "succ_LimitE";
     1.7 +AddSEs [succ_LimitE];
     1.8 +
     1.9 +Goal "~ Limit(succ(i))";
    1.10 +by (Blast_tac 1);
    1.11 +qed "not_succ_Limit";
    1.12 +Addsimps [not_succ_Limit];
    1.13  
    1.14  Goal "[| Limit(i);  i le succ(j) |] ==> i le j";
    1.15 -by (safe_tac (claset() addSEs [succ_LimitE, leE]));
    1.16 +by (blast_tac (claset() addSEs [leE]) 1);
    1.17  qed "Limit_le_succD";
    1.18  
    1.19  (** Traditional 3-way case analysis on ordinals **)