# HG changeset patch
# User paulson
# Date 1009046776 -3600
# Node ID 5b9b0adca8aa5cdc94c1df6713837d66e205acae
# Parent  cd35fe5947d41e13cdad100c2c258546e1d34e44
tweaked the standard theorems

diff -r cd35fe5947d4 -r 5b9b0adca8aa src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Sat Dec 22 19:42:35 2001 +0100
+++ b/src/ZF/Ordinal.ML	Sat Dec 22 19:46:16 2001 +0100
@@ -691,9 +691,15 @@
 by (assume_tac 1);
 by (etac (Limit_is_Ord RS Ord_succD RS le_refl) 1);
 qed "succ_LimitE";
+AddSEs [succ_LimitE];
+
+Goal "~ Limit(succ(i))";
+by (Blast_tac 1);
+qed "not_succ_Limit";
+Addsimps [not_succ_Limit];
 
 Goal "[| Limit(i);  i le succ(j) |] ==> i le j";
-by (safe_tac (claset() addSEs [succ_LimitE, leE]));
+by (blast_tac (claset() addSEs [leE]) 1);
 qed "Limit_le_succD";
 
 (** Traditional 3-way case analysis on ordinals **)