changeset 68 | acad709cad5d |
parent 63 | 94436622324d |
--- 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