src/HOL/Arith.thy
changeset 1796 c42db9ab8728
parent 1475 7f5a4cd08209
child 1824 44254696843a
--- 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