src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy

  apply(rule disjI2, clarify, erule less_SucE, force)
  apply(case_tac "M x!snd(E x! ind x)=Black")
   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)
 apply(disjE_tac)
  apply (simp_all)

 apply interfree_aux
 apply(simp_all add:mul_collector_mutator_interfree)
 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 *}
 
 text {* The total number of verification conditions is 328 *}