src/HOL/Real/Hyperreal/Series.ML

--- a/src/HOL/Real/Hyperreal/Series.ML	Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML	Tue Dec 19 15:06:59 2000 +0100
@@ -260,12 +260,6 @@
 qed "sumr_group";
 Addsimps [sumr_group];
 
-Goal "0 < (k::nat) --> ~(n*k < n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "lemma_summable_group";
-Addsimps [lemma_summable_group];
-
 (*-------------------------------------------------------------------
                         Infinite sums
     Theorems follow from properties of limits and sums