Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Extend.thy
changeset 69313 b021008c5397
parent 67613 ce654b0e6d69
child 69597 ff784d5a5bfb 
--- a/src/HOL/UNITY/Extend.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Extend.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -249,7 +249,7 @@
 lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
   by auto
 
-lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
+lemma extend_set_INT_distrib: "extend_set h (\<Inter>(B ` A)) = (\<Inter>x \<in> A. extend_set h (B x))"
   by auto
 
 lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
isabelle