diff -r fc54d5fc4a7a -r 838c66e760b5 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Divides.thy	Thu May 17 19:49:16 2007 +0200
@@ -8,6 +8,7 @@
 
 theory Divides
 imports Datatype Power
+uses "~~/src/Provers/Arith/cancel_div_mod.ML"
 begin
 
 (*We use the same class for div and mod;
@@ -31,11 +32,11 @@
 notation
   mod (infixl "mod" 70)
 
-instance nat :: "Divides.div"
+instance nat :: Divides.div
+  div_def: "m div n == wfrec (pred_nat^+)
+                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
   mod_def: "m mod n == wfrec (pred_nat^+)
-                          (%f j. if j<n | n=0 then j else f (j-n)) m"
-  div_def: "m div n == wfrec (pred_nat^+)
-                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
+                          (%f j. if j<n | n=0 then j else f (j-n)) m" ..
 
 definition
   (*The definition of dvd is polymorphic!*)