changeset 69313 | b021008c5397 |
parent 64267 | b9a1486e79be |
child 75450 | f16d83de3e4a |
--- a/src/HOL/Library/Set_Algebras.thy Sun Nov 18 09:51:41 2018 +0100 +++ b/src/HOL/Library/Set_Algebras.thy Sun Nov 18 18:07:51 2018 +0000 @@ -408,8 +408,8 @@ by (auto simp: set_times_def) lemma set_times_UNION_distrib: - "A * UNION I M = (\<Union>i\<in>I. A * M i)" - "UNION I M * A = (\<Union>i\<in>I. M i * A)" + "A * \<Union>(M ` I) = (\<Union>i\<in>I. A * M i)" + "\<Union>(M ` I) * A = (\<Union>i\<in>I. M i * A)" by (auto simp: set_times_def) end