author  paulson 
Mon, 08 May 2000 16:59:18 +0200  
changeset 8836  32fe62227ff0 
parent 8356  14d89313c66c 
permissions  rwrr 
8836  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 
8836  12 
sum_0 "sum f 0 = 0" 
13 
sum_Suc "sum f (Suc n) = f(n) + sum f n" 

3269  14 

969  15 
end 