src/HOL/PreList.thy
changeset 13297 e4ae0732e2be
parent 12919 d6a0d168291e
child 13878 90ca3815e4b2
--- 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