--- a/src/ZF/Arith.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Arith.thy Fri Oct 10 18:23:31 1997 +0200
@@ -18,8 +18,8 @@
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))"
- diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
+ add_def "m#+n == rec(m, n, %u v. succ(v))"
+ diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y. x))"
mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
mod_def "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
div_def "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"