src/HOL/Hoare_Parallel/RG_Hoare.thy
changeset 69313 b021008c5397
parent 68975 5ce4d117cea7
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -1134,7 +1134,7 @@
     1.4   apply(drule_tac c="s" in subsetD,simp)
     1.5   apply simp
     1.6  apply clarify
     1.7 -apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> UNION (S j) (T j) \<subseteq> (L j)" for H M S T L in allE)
     1.8 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> \<Union>((T j) ` (S j)) \<subseteq> (L j)" for H M S T L in allE)
     1.9  apply simp
    1.10  apply(erule subsetD)
    1.11  apply simp