author  clasohm 
Mon, 05 Feb 1996 21:29:06 +0100  
changeset 1476  608483c2122a 
parent 1376  92f83b9d17e1 
child 3269  eca2a3634acd 
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 
969  11 
rules sum_0 "sum f 0 = 0" 
12 
sum_Suc "sum f (Suc n) = f(n) + sum f n" 

13 
end 