# HG changeset patch
# User obua
# Date 1101232739 -3600
# Node ID e9669e0d6452225a19bd46f806092887d371b71e
# Parent  ebdd193e15ec10353a99fdb6ffcaf8cd2e7a02f3
prettier proof of setsum_diff

diff -r ebdd193e15ec -r e9669e0d6452 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Nov 23 17:47:37 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 23 18:58:59 2004 +0100
@@ -1009,18 +1009,14 @@
   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
 proof -
   from le have finiteB: "finite B" using finite_subset by auto
-  show ?thesis using le finiteB
-    proof (induct rule: Finites.induct[OF finiteB])
-      case 1
+  show ?thesis using finiteB le
+    proof (induct)
+      case empty
       thus ?case by auto
     next
-      case 2
-      thus ?case using le 
-	apply auto
-	apply (subst Diff_insert)
-	apply (subst setsum_diff1)
-	apply (auto simp add: insert_absorb)
-	done
+      case (insert F x)
+      thus ?case using le finiteB 
+	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
     qed
   qed