src/HOL/Divides.thy
changeset 7029 08d4eb8500dd
parent 6865 5577ffe4c2f1
child 8902 a705822f4e2a
     1.1 --- a/src/HOL/Divides.thy	Sun Jul 18 11:06:08 1999 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Jul 19 15:18:16 1999 +0200
     1.3 @@ -28,10 +28,10 @@
     1.4  defs
     1.5  
     1.6    mod_def   "m mod n == wfrec (trancl pred_nat)
     1.7 -                          (%f j. if j<n then j else f (j-n)) m"
     1.8 +                          (%f j. if j<n | n=0 then j else f (j-n)) m"
     1.9  
    1.10    div_def   "m div n == wfrec (trancl pred_nat) 
    1.11 -                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
    1.12 +                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    1.13  
    1.14  (*The definition of dvd is polymorphic!*)
    1.15    dvd_def   "m dvd n == EX k. n = m*k"