changeset 45922 | 63cc69265acf |
parent 44227 | 78e033e8ba05 |
child 49739 | 13aa6d8268ec |
--- 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}"