# HG changeset patch
# User lcp
# Date 766920512 -7200
# Node ID acad709cad5de6f20beaaa9d71ea4bd63974c058
# Parent  bea4ea9128385e6a3c8d1b0dd05c583315578eb9
tidied definitions and proofs

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
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