author  paulson 
Wed, 08 Mar 2000 16:24:46 +0100  
changeset 8356  14d89313c66c 
parent 5184  9b8547a9496a 
child 8836  32fe62227ff0 
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 

8356  9 
NatSum = Main + 
1376  10 
consts sum :: [nat=>nat, nat] => nat 
5184  11 
primrec 
3269  12 
"sum f 0 = 0" 
13 
"sum f (Suc n) = f(n) + sum f n" 

14 

969  15 
end 