Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Arith.thy
changeset 753 ec86863e87c8
parent 124 858ab9a9b047
child 1401 0c439768f45c 
--- a/src/ZF/Arith.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Arith.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
     "#+" :: "[i,i]=>i"      		(infixl 65)
     "#-" :: "[i,i]=>i"      		(infixl 65)
 
-rules
+defs
     rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
     add_def  "m#+n == rec(m, n, %u v.succ(v))"
isabelle