author  clasohm 
Wed, 22 Mar 1995 12:42:34 +0100  
changeset 969  b051e2fc2e34 
child 1376  92f83b9d17e1 
permissions  rwrr 
969  1 
(* Title: HOL/ex/natsum.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

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 + 

10 
consts sum :: "[nat=>nat, nat] => nat" 

11 
rules sum_0 "sum f 0 = 0" 

12 
sum_Suc "sum f (Suc n) = f(n) + sum f n" 

13 
end 