--- a/src/HOL/Divides.thy Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/Divides.thy Fri Oct 30 18:32:40 2009 +0100
@@ -131,7 +131,7 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0"
proof
assume "b mod a = 0"
with mod_div_equality [of b a] have "b div a * a = b" by simp
@@ -2460,4 +2460,13 @@
then show ?thesis by (simp add: divmod_int_pdivmod)
qed
+code_modulename SML
+ Divides Arith
+
+code_modulename OCaml
+ Divides Arith
+
+code_modulename Haskell
+ Divides Arith
+
end