# HG changeset patch
# User haftmann
# Date 1259144217 -3600
# Node ID 53993394ac19a8e0bad14a6a960ed47f5dc210b5
# Parent  2afc55e8ed27ce483cfe3813c8e6958df388a883
tuned

diff -r 2afc55e8ed27 -r 53993394ac19 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Nov 25 11:16:57 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Nov 25 11:16:57 2009 +0100
@@ -6,7 +6,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Nat Product_Type Power
+imports Power Product_Type Sum_Type
 begin
 
 subsection {* Definition and basic properties *}
@@ -1157,8 +1157,8 @@
    ==> setsum (%x. f x) A = setsum (%x. g x) B"
 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
 
-lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
-by (rule setsum_cong[OF refl], auto);
+lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
+by (rule setsum_cong[OF refl], auto)
 
 lemma setsum_reindex_cong:
    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]