src/HOL/Library/Stream.thy
changeset 69313 b021008c5397
parent 68406 6beb45f6cf67
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Library/Stream.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Stream.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -510,10 +510,10 @@
     1.4          intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
     1.5  qed
     1.6  
     1.7 -lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
     1.8 +lemma sset_smerge: "sset (smerge ss) = \<Union>(sset ` (sset ss))"
     1.9  proof safe
    1.10    fix x assume "x \<in> sset (smerge ss)"
    1.11 -  thus "x \<in> UNION (sset ss) sset"
    1.12 +  thus "x \<in> \<Union>(sset ` (sset ss))"
    1.13      unfolding smerge_def by (subst (asm) sset_flat)
    1.14        (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
    1.15  next