src/HOL/Hyperreal/Series.thy
changeset 15053 405be2b48f5b
parent 15047 fa62de5862b9
child 15085 5693a977a767
--- a/src/HOL/Hyperreal/Series.thy	Fri Jul 16 11:46:59 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Fri Jul 16 17:31:44 2004 +0200
@@ -24,10 +24,6 @@
    "suminf f == (@s. f sums s)"
 
 
-text{*This simprule replaces @{text "sumr 0 n"} by a term involving 
-  @{term lessThan}, making other simprules inapplicable.*}
-declare atLeast0LessThan [simp del]
-
 lemma sumr_Suc [simp]:
      "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
 by (simp add: atLeastLessThanSuc)