src/HOL/Big_Operators.thy
changeset 40786 0a54cfc9add3
parent 39302 d7728f65b353
child 41550 efa734d9b221
     1.1 --- a/src/HOL/Big_Operators.thy	Sat Nov 27 17:44:36 2010 -0800
     1.2 +++ b/src/HOL/Big_Operators.thy	Sun Nov 28 15:20:51 2010 +0100
     1.3 @@ -707,7 +707,7 @@
     1.4  proof -
     1.5    have "A <+> B = Inl ` A \<union> Inr ` B" by auto
     1.6    moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
     1.7 -    by(auto intro: finite_imageI)
     1.8 +    by auto
     1.9    moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
    1.10    moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
    1.11    ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)