# HG changeset patch
# User paulson
# Date 834747779 -7200
# Node ID c42db9ab8728a2e34b43ae0e466aacc3757c4ad1
# Parent  0466f9668ba345bf701ada5fbba3570f03f399b5
Tidied spacing

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