src/HOL/NatArith.thy

--- a/src/HOL/NatArith.thy	Mon Jul 12 19:56:58 2004 +0200
+++ b/src/HOL/NatArith.thy	Tue Jul 13 12:32:01 2004 +0200
@@ -36,7 +36,7 @@
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
-
+(*
 subsection {* Generic summation indexed over natural numbers *}
 
 consts
@@ -53,5 +53,5 @@
 theorem Summation_step:
     "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
   by (induct n) simp_all
-
+*)
 end