# HG changeset patch
# User paulson
# Date 959766988 -7200
# Node ID 45c3c2cf238630e116b03131954c155f055e5d59
# Parent  3747ec2aeb866236d8c5873481f5ea1cfdc42c9d
moved some theorems to Finite.ML

diff -r 3747ec2aeb86 -r 45c3c2cf2386 src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Wed May 31 11:55:51 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Wed May 31 11:56:28 2000 +0200
@@ -292,23 +292,6 @@
 
 (** Towards the induction rule **)
 
-Goal "finite F ==> (setsum f F = 0) = (! a:F. f a = (0::nat))";
-by (etac finite_induct 1);
-by Auto_tac;
-qed "setsum_0";
-Addsimps [setsum_0];
-
-Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
-by (etac finite_induct 1);
-by Auto_tac;
-no_qed();
-val lemma = result();
-
-Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
-by (dtac lemma 1);
-by (Fast_tac 1);
-qed "setsum_SucD";
-
 Goal "[| finite F; 0 < f a |] ==> \
 \     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
 by (etac finite_induct 1);