src/HOL/Hoare_Parallel/Gar_Coll.thy
changeset 32687 27530efec97a
parent 32621 a073cb249a06
child 34233 156c42518cfc
     1.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 11:01:49 2009 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 12:23:52 2009 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4      \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
     1.5  apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
     1.6  apply annhoare
     1.7 -apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
     1.8 +apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
     1.9         apply force
    1.10        apply force
    1.11       apply force
    1.12 @@ -297,8 +297,6 @@
    1.13  apply(erule subset_psubset_trans)
    1.14  apply(erule Graph11)
    1.15  apply fast
    1.16 ---{* 3 subgoals left *}
    1.17 -apply force
    1.18  --{* 2 subgoals left *}
    1.19  apply clarify
    1.20  apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)