author  paulson 
Wed, 21 May 1997 10:55:21 +0200  
changeset 3269  eca2a3634acd 
parent 1476  608483c2122a 
child 5184  9b8547a9496a 
permissions  rwrr 
1476  1 
(* Title: HOL/ex/natsum.thy 
969  2 
ID: $Id$ 
1476  3 
Author: Tobias Nipkow 
969  4 
Copyright 1994 TU Muenchen 
5 

6 
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. 

7 
*) 

8 

9 
NatSum = Arith + 

1376  10 
consts sum :: [nat=>nat, nat] => nat 
3269  11 
primrec "sum" nat 
12 
"sum f 0 = 0" 

13 
"sum f (Suc n) = f(n) + sum f n" 

14 

969  15 
end 