src/HOL/Library/Set_Algebras.thy
changeset 69313 b021008c5397
parent 64267 b9a1486e79be
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -408,8 +408,8 @@
     1.4    by (auto simp: set_times_def)
     1.5  
     1.6  lemma set_times_UNION_distrib:
     1.7 -  "A * UNION I M = (\<Union>i\<in>I. A * M i)"
     1.8 -  "UNION I M * A = (\<Union>i\<in>I. M i * A)"
     1.9 +  "A * \<Union>(M ` I) = (\<Union>i\<in>I. A * M i)"
    1.10 +  "\<Union>(M ` I) * A = (\<Union>i\<in>I. M i * A)"
    1.11    by (auto simp: set_times_def)
    1.12  
    1.13  end