--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Thu Sep 24 19:14:18 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri Sep 25 09:50:31 2009 +0200
@@ -253,7 +253,7 @@
\<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
apply (unfold Propagate_Black_def PBInv_def Auxk_def collector_defs)
apply annhoare
-apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
+apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
apply force
apply force
apply force
@@ -297,8 +297,6 @@
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
---{* 3 subgoals left *}
-apply force
--{* 2 subgoals left *}
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)