codegen
authornipkow
Thu Dec 11 08:56:02 2008 +0100 (2008-12-11)
changeset 2910812ca66b887a0
parent 29107 e70b9c2bee14
child 29109 389ebed8b98e
codegen
src/HOL/Divides.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Dec 11 08:53:53 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 11 08:56:02 2008 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4    note that ultimately show thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.8 +lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.9  proof
    1.10    assume "b mod a = 0"
    1.11    with mod_div_equality [of b a] have "b div a * a = b" by simp
     2.1 --- a/src/HOL/Real.thy	Thu Dec 11 08:53:53 2008 +0100
     2.2 +++ b/src/HOL/Real.thy	Thu Dec 11 08:56:02 2008 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Real
     2.5 -imports "~~/src/HOL/Real/RealVector"
     2.6 +imports RComplete "~~/src/HOL/Real/RealVector"
     2.7  begin
     2.8  
     2.9  end