--- a/src/HOL/Divides.thy Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Divides.thy Sat Sep 29 08:58:51 2007 +0200
@@ -29,7 +29,7 @@
[code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
class dvd_mod = times + div + zero + -- {* for code generation *}
- assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
+ assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
definition
quorem :: "(nat*nat) * (nat*nat) => bool" where
@@ -880,8 +880,6 @@
qed
-
-
subsection {* Code generation for div, mod and dvd on nat *}
definition [code func del]: