src/HOL/Divides.thy
changeset 33364 2bd12592c5e8
parent 33361 1f18de40b43f
child 33728 cb4235333c30
     1.1 --- a/src/HOL/Divides.thy	Fri Oct 30 14:02:42 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 30 18:32:40 2009 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4    note that ultimately show thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.8 +lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "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
    1.12 @@ -2460,4 +2460,13 @@
    1.13    then show ?thesis by (simp add: divmod_int_pdivmod)
    1.14  qed
    1.15  
    1.16 +code_modulename SML
    1.17 +  Divides Arith
    1.18 +
    1.19 +code_modulename OCaml
    1.20 +  Divides Arith
    1.21 +
    1.22 +code_modulename Haskell
    1.23 +  Divides Arith
    1.24 +
    1.25  end