diff -r 0466f9668ba3 -r c42db9ab8728 src/HOL/Arith.thy
--- 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