--- a/src/HOL/Arith.thy Fri Jun 14 12:22:42 1996 +0200
+++ b/src/HOL/Arith.thy Fri Jun 14 12:22:59 1996 +0200
@@ -20,9 +20,10 @@
add_def "m+n == nat_rec m n (%u v. Suc(v))"
diff_def "m-n == nat_rec n m (%u v. pred(v))"
mult_def "m*n == nat_rec m 0 (%u v. n + v)"
-mod_def "m mod n == wfrec (trancl pred_nat)
+
+ mod_def "m mod n == wfrec (trancl pred_nat)
(%f j. if j<n then j else f (j-n)) m"
-div_def "m div n == wfrec (trancl pred_nat)
+ div_def "m div n == wfrec (trancl pred_nat)
(%f j. if j<n then 0 else Suc (f (j-n))) m"
end