Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tidied definitions and proofs
authorlcp
Thu, 21 Apr 1994 11:28:32 +0200
changeset 68 acad709cad5d
parent 67 bea4ea912838
child 69 44b82132fe82
tidied definitions and proofs
ex/NatSum.thy file | annotate | diff | comparison | revisions
ex/natsum.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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
Old_HOL