src/HOL/Arith.thy
changeset 965 24eef3860714
parent 923 ff1574a81019
child 972 e61b058d58d2
     1.1 --- a/src/HOL/Arith.thy	Fri Mar 17 22:46:26 1995 +0100
     1.2 +++ b/src/HOL/Arith.thy	Mon Mar 20 15:35:28 1995 +0100
     1.3 @@ -20,8 +20,8 @@
     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) j (f (j-n))))"
     1.8 -  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.(if (j<n) 0 (Suc (f (j-n)))))"
     1.9 +  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
    1.10 +  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
    1.11  end
    1.12  
    1.13  (*"Difference" is subtraction of natural numbers.