--- a/src/HOL/Divides.thy Thu Dec 11 08:53:53 2008 +0100
+++ b/src/HOL/Divides.thy Thu Dec 11 08:56:02 2008 +0100
@@ -127,7 +127,7 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code unfold]: "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
--- a/src/HOL/Real.thy Thu Dec 11 08:53:53 2008 +0100
+++ b/src/HOL/Real.thy Thu Dec 11 08:56:02 2008 +0100
@@ -1,5 +1,5 @@
theory Real
-imports "~~/src/HOL/Real/RealVector"
+imports RComplete "~~/src/HOL/Real/RealVector"
begin
end