src/HOL/Divides.thy
changeset 22916 8caf6da610e2
parent 22845 5f9138bcb3d7
child 22993 838c66e760b5
     1.1 --- a/src/HOL/Divides.thy	Thu May 10 04:06:56 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu May 10 10:21:44 2007 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  instance nat :: "Divides.div"
     1.5    mod_def: "m mod n == wfrec (pred_nat^+)
     1.6                            (%f j. if j<n | n=0 then j else f (j-n)) m"
     1.7 -  div_def:   "m div n == wfrec (pred_nat^+)
     1.8 +  div_def: "m div n == wfrec (pred_nat^+)
     1.9                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.10  
    1.11  definition