src/HOL/Finite_Set.thy
changeset 15318 e9669e0d6452
parent 15315 a358e31572d9
child 15327 0230a10582d3
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 23 17:47:37 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 23 18:58:59 2004 +0100
     1.3 @@ -1009,18 +1009,14 @@
     1.4    shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
     1.5  proof -
     1.6    from le have finiteB: "finite B" using finite_subset by auto
     1.7 -  show ?thesis using le finiteB
     1.8 -    proof (induct rule: Finites.induct[OF finiteB])
     1.9 -      case 1
    1.10 +  show ?thesis using finiteB le
    1.11 +    proof (induct)
    1.12 +      case empty
    1.13        thus ?case by auto
    1.14      next
    1.15 -      case 2
    1.16 -      thus ?case using le 
    1.17 -	apply auto
    1.18 -	apply (subst Diff_insert)
    1.19 -	apply (subst setsum_diff1)
    1.20 -	apply (auto simp add: insert_absorb)
    1.21 -	done
    1.22 +      case (insert F x)
    1.23 +      thus ?case using le finiteB 
    1.24 +	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
    1.25      qed
    1.26    qed
    1.27