changeset 1376 | 92f83b9d17e1 |
parent 969 | b051e2fc2e34 |
child 1476 | 608483c2122a |
--- a/src/HOL/ex/NatSum.thy Thu Nov 30 12:58:44 1995 +0100 +++ b/src/HOL/ex/NatSum.thy Fri Dec 01 12:03:13 1995 +0100 @@ -7,7 +7,7 @@ *) NatSum = Arith + -consts sum :: "[nat=>nat, nat] => nat" +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