src/HOL/Hoare_Parallel/Gar_Coll.thy

 --{* 20 subgoals left *}
 apply(tactic{* TRYALL (clarify_tac @{context}) *})
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 apply(tactic {* TRYALL (etac disjE) *})
 apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *})
 apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
 apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
 done
 
 subsubsection {* Interference freedom Mutator-Collector *}