src/HOL/ex/NatSum.thy
changeset 5184 9b8547a9496a
parent 3269 eca2a3634acd
child 8356 14d89313c66c
--- a/src/HOL/ex/NatSum.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/NatSum.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -8,7 +8,7 @@
 
 NatSum = Arith +
 consts sum     :: [nat=>nat, nat] => nat
-primrec "sum" nat 
+primrec 
   "sum f 0 = 0"
   "sum f (Suc n) = f(n) + sum f n"