src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Sun Jul 18 11:06:08 1999 +0200
+++ b/src/HOL/Divides.thy	Mon Jul 19 15:18:16 1999 +0200
@@ -28,10 +28,10 @@
 defs
 
   mod_def   "m mod n == wfrec (trancl pred_nat)
-                          (%f j. if j<n then j else f (j-n)) m"
+                          (%f j. if j<n | n=0 then j else f (j-n)) m"
 
   div_def   "m div n == wfrec (trancl pred_nat) 
-                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
+                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
 
 (*The definition of dvd is polymorphic!*)
   dvd_def   "m dvd n == EX k. n = m*k"