Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorbulwahn
Tue, 20 Dec 2011 14:43:42 +0100
changeset 45922 63cc69265acf
parent 45921 28831430f230
child 45923 473b744c23f2
tuned
src/HOL/Library/Permutations.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Permutations.thy	Tue Dec 20 14:43:41 2011 +0100
+++ b/src/HOL/Library/Permutations.thy	Tue Dec 20 14:43:42 2011 +0100
@@ -742,7 +742,6 @@
 apply metis
 done
 
-term setsum
 lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
 proof-
   let ?S = "{p . p permutes S}"
isabelle