1.1 --- a/src/HOL/PreList.thy	Thu Jul 04 15:06:46 2002 +0200
     1.2 +++ b/src/HOL/PreList.thy	Thu Jul 04 16:48:21 2002 +0200
     1.3 @@ -19,22 +19,4 @@
     1.4  (*belongs to theory Wellfounded_Recursion*)
     1.5  lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
     1.6  
     1.7 -
     1.8 -(* generic summation indexed over nat *)
     1.9 -
    1.10 -consts
    1.11 -  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
    1.12 -primrec
    1.13 -  "Summation f 0 = 0"
    1.14 -  "Summation f (Suc n) = Summation f n + f n"
    1.15 -
    1.16 -syntax
    1.17 -  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    1.18 -translations
    1.19 -  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
    1.20 -
    1.21 -theorem Summation_step:
    1.22 -    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    1.23 -  by (induct n) simp_all
    1.24 -
    1.25  end