author  berghofe 
Fri, 24 Jul 1998 13:19:38 +0200  
changeset 5184  9b8547a9496a 
parent 3269  eca2a3634acd 
child 8356  14d89313c66c 
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 
5184  11 
primrec 
3269  12 
"sum f 0 = 0" 
13 
"sum f (Suc n) = f(n) + sum f n" 

14 

969  15 
end 