src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
changeset 32687 27530efec97a
parent 32621 a073cb249a06
child 32960 69916a850301
     1.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 11:01:49 2009 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 12:23:52 2009 +0200
     1.3 @@ -276,8 +276,6 @@
     1.4    apply(force)
     1.5   apply(force)
     1.6  apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
     1.7 ---{* 3 subgoals left *}
     1.8 -apply force
     1.9  --{* 2 subgoals left *}
    1.10  apply clarify
    1.11  apply(conjI_tac)
    1.12 @@ -1235,9 +1233,9 @@
    1.13  apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
    1.14  apply(tactic  {* TRYALL (interfree_aux_tac) *})
    1.15  --{* 76 subgoals left *}
    1.16 -apply (clarify,simp add: nth_list_update)+
    1.17 +apply (clarsimp simp add: nth_list_update)+
    1.18  --{* 56 subgoals left *}
    1.19 -apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
    1.20 +apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
    1.21  done
    1.22  
    1.23  subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}