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)"