ex/natsum.thy
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