--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Thu Sep 24 19:14:18 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri Sep 25 09:50:31 2009 +0200
@@ -276,8 +276,6 @@
apply(force)
apply(force)
apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 3 subgoals left *}
-apply force
--{* 2 subgoals left *}
apply clarify
apply(conjI_tac)
@@ -1235,9 +1233,9 @@
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
apply(tactic {* TRYALL (interfree_aux_tac) *})
--{* 76 subgoals left *}
-apply (clarify,simp add: nth_list_update)+
+apply (clarsimp simp add: nth_list_update)+
--{* 56 subgoals left *}
-apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
+apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
done
subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}