Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Divides.thy
changeset 22916 8caf6da610e2
parent 22845 5f9138bcb3d7
child 22993 838c66e760b5 
--- a/src/HOL/Divides.thy	Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Divides.thy	Thu May 10 10:21:44 2007 +0200
@@ -34,7 +34,7 @@
 instance nat :: "Divides.div"
   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^+)
+  div_def: "m div n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
 
 definition
isabelle