src/HOL/UNITY/Extend.thy
changeset 69313 b021008c5397
parent 67613 ce654b0e6d69
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/UNITY/Extend.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -249,7 +249,7 @@
     1.4  lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
     1.5    by auto
     1.6  
     1.7 -lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
     1.8 +lemma extend_set_INT_distrib: "extend_set h (\<Inter>(B ` A)) = (\<Inter>x \<in> A. extend_set h (B x))"
     1.9    by auto
    1.10  
    1.11  lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"