# HG changeset patch
# User paulson
# Date 905442576 -7200
# Node ID 746cd24ee3acce88aad6d80dd1d687b3bfb37fff
# Parent  a4c9eaff23336436fabc857ef50f9509cbf7fcf7
tidied

diff -r a4c9eaff2333 -r 746cd24ee3ac src/ZF/AC/WO1_WO6.ML
--- a/src/ZF/AC/WO1_WO6.ML	Thu Sep 10 17:49:14 1998 +0200
+++ b/src/ZF/AC/WO1_WO6.ML	Thu Sep 10 17:49:36 1998 +0200
@@ -62,20 +62,20 @@
 (* ********************************************************************** *)
 
 Goalw WO_defs "[| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
-by (fast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
+by (rtac allI 1);
+by (dtac spec 1);
+by (blast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
 qed "WO4_mono";
 
 (* ********************************************************************** *)
 
 Goalw WO_defs "[| m:nat; 1 le m; WO4(m) |] ==> WO5";
-    (*ZF_cs is essential: default claset's too slow*)
-by (fast_tac ZF_cs 1);
+by (Blast_tac 1);
 qed "WO4_WO5";
 
 (* ********************************************************************** *)
 
 Goalw WO_defs "WO5 ==> WO6";
-    (*ZF_cs is essential: default claset's too slow*)
-by (fast_tac ZF_cs 1);
+by (Blast_tac 1);
 qed "WO5_WO6";