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/Algebra/FiniteProduct.thy
changeset 58860 fee7cfa69c50
parent 56142 8bb21318e10b
child 60112 3eab4acaa035 
--- a/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -33,7 +33,7 @@
 
 lemma foldSetD_closed:
   "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
-      |] ==> z \<in> D";
+      |] ==> z \<in> D"
   by (erule foldSetD.cases) auto
 
 lemma Diff1_foldSetD:
@@ -72,7 +72,7 @@
   and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D"
 
 lemma (in LCD) foldSetD_closed [dest]:
-  "(A, z) \<in> foldSetD D f e ==> z \<in> D";
+  "(A, z) \<in> foldSetD D f e ==> z \<in> D"
   by (erule foldSetD.cases) auto
 
 lemma (in LCD) Diff1_foldSetD:
isabelle