diff -r bea4ea912838 -r acad709cad5d ex/natsum.thy --- a/ex/natsum.thy Thu Apr 21 11:13:22 1994 +0200 +++ b/ex/natsum.thy Thu Apr 21 11:28:32 1994 +0200 @@ -7,7 +7,7 @@ *) NatSum = Arith + -consts sum :: "[nat=>nat, nat] => nat" -rules sum_0 "sum(f,0) = 0" - sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" +consts sum :: "[nat=>nat, nat] => nat" +rules sum_0 "sum(f,0) = 0" + sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" end