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/Library/Formal_Power_Series.thy
changeset 44174 d1d79f0e1ea6
parent 41959 b460124855b8
child 46131 ab07a3ef821c 
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -1436,7 +1436,7 @@
       apply (rule setsum_cong2) by (simp del: replicate.simps)
     also have "\<dots> = n" using i by (simp add: setsum_delta)
     finally
-    have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def
+    have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
       by blast
     then have "?xs \<in> ?A"  using nxs  by blast}
   ultimately show ?thesis by auto
isabelle