# HG changeset patch
# User paulson
# Date 882874303 -3600
# Node ID 09864e2536d3514ada516bac5ca94a7f62ac3b2d
# Parent  3a43a694d53b75a17f36852b240cd972f1df074c
Now Blast_tac works properly

diff -r 3a43a694d53b -r 09864e2536d3 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Tue Dec 23 11:50:36 1997 +0100
+++ b/src/ZF/Ordinal.ML	Tue Dec 23 11:51:43 1997 +0100
@@ -518,7 +518,7 @@
 (*Identical to  succ(i) < succ(j) ==> i<j  *)
 goal Ordinal.thy "!!i j. succ(i) le j ==> i<j";
 by (rtac (not_le_iff_lt RS iffD1) 1);
-by (fast_tac le_cs 3);
+by (blast_tac le_cs 3);
 by (ALLGOALS (blast_tac (claset() addEs [ltE, make_elim Ord_succD])));
 qed "succ_leE";