src/HOL/NumberTheory/Finite2.thy
changeset 15109 bba563cdd997
parent 15047 fa62de5862b9
child 15392 290bc97038c7
     1.1 --- a/src/HOL/NumberTheory/Finite2.thy	Wed Aug 04 19:09:41 2004 +0200
     1.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Wed Aug 04 19:09:58 2004 +0200
     1.3 @@ -266,13 +266,7 @@
     1.4  
     1.5  lemma sum_prop [rule_format]: "finite B ==>
     1.6                    inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
     1.7 -apply (rule finite_induct, assumption, force)
     1.8 -apply (rule impI, auto)
     1.9 -apply (simp add: inj_on_def)
    1.10 -apply (subgoal_tac "f x \<notin> f ` F")
    1.11 -apply (subgoal_tac "finite (f ` F)");
    1.12 -apply (auto simp add: setsum_insert)
    1.13 -by (simp add: inj_on_def) 
    1.14 +by (rule finite_induct, auto)
    1.15  
    1.16  lemma sum_prop_id: "finite B ==> inj_on f B ==> 
    1.17      setsum f B = setsum id (f ` B)";