--- a/src/HOL/PreList.thy Thu Jul 04 15:06:46 2002 +0200
+++ b/src/HOL/PreList.thy Thu Jul 04 16:48:21 2002 +0200
@@ -19,22 +19,4 @@
(*belongs to theory Wellfounded_Recursion*)
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
-
-(* generic summation indexed over nat *)
-
-consts
- Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
-primrec
- "Summation f 0 = 0"
- "Summation f (Suc n) = Summation f n + f n"
-
-syntax
- "_Summation" :: "idt => nat => 'a => nat" ("\<Sum>_<_. _" [0, 51, 10] 10)
-translations
- "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
-
-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