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 22845 5f9138bcb3d7
parent 22800 eaf5e7ef35d9
child 22916 8caf6da610e2 
--- a/src/HOL/Divides.thy	Sun May 06 21:49:44 2007 +0200
+++ b/src/HOL/Divides.thy	Sun May 06 21:50:17 2007 +0200
@@ -898,7 +898,7 @@
 
 subsection {* Code generation for div, mod and dvd on nat *}
 
-definition [code nofunc]:
+definition [code func del]:
   "divmod (m\<Colon>nat) n = (m div n, m mod n)"
 
 lemma divmod_zero [code]: "divmod m 0 = (0, m)"
isabelle