src/HOL/Arith.thy
changeset 1475 7f5a4cd08209
parent 1370 7361ac9b024d
child 1796 c42db9ab8728
     1.1 --- a/src/HOL/Arith.thy	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/Arith.thy	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -20,8 +20,10 @@
     1.4    add_def   "m+n == nat_rec m n (%u v. Suc(v))"
     1.5    diff_def  "m-n == nat_rec n m (%u v. pred(v))"
     1.6    mult_def  "m*n == nat_rec m 0 (%u v. n + v)"
     1.7 -  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
     1.8 -  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
     1.9 +mod_def "m mod n == wfrec (trancl pred_nat)
    1.10 +                          (%f j. if j<n then j else f (j-n)) m"
    1.11 +div_def "m div n == wfrec (trancl pred_nat) 
    1.12 +                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
    1.13  end
    1.14  
    1.15  (*"Difference" is subtraction of natural numbers.