--- a/src/HOL/UNITY/WFair.ML Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Fri Sep 11 16:25:40 1998 +0200
@@ -172,7 +172,6 @@
Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
\ ==> leadsTo acts B B'";
-(*PROOF FAILED unless leadsTo_Trans is last*)
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
leadsTo_Trans]) 1);
qed "leadsTo_weaken";
@@ -490,8 +489,7 @@
by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD,
subset_imp_leadsTo]) 2);
-(*addIs looks safer, but loops with PROOF FAILED*)
-by (blast_tac (claset() addSIs [leadsTo_Trans]) 1);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "stable_completion";