src/HOL/Finite_Set.thy

 *)
 
 header {* Finite sets *}
 
 theory Finite_Set
-imports Nat Product_Type Power
+imports Power Product_Type Sum_Type
 begin
 
 subsection {* Definition and basic properties *}
 
 inductive finite :: "'a set => bool"

 lemma strong_setsum_cong[cong]:
   "A = B ==> (!!x. x:B =simp=> f x = g x)
    ==> 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)|] 
     ==> setsum h B = setsum g A"
 by (simp add: setsum_reindex cong: setsum_cong)