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

     2.1 --- a/src/HOL/HOL.thy	Fri Oct 30 14:02:42 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Fri Oct 30 18:32:40 2009 +0100
     2.3 @@ -1818,7 +1818,7 @@
     2.4  
     2.5  code_datatype "TYPE('a\<Colon>{})"
     2.6  
     2.7 -code_datatype Trueprop "prop"
     2.8 +code_datatype "prop" Trueprop
     2.9  
    2.10  text {* Code equations *}
    2.11  

     3.1 --- a/src/HOL/Int.thy	Fri Oct 30 14:02:42 2009 +0100
     3.2 +++ b/src/HOL/Int.thy	Fri Oct 30 18:32:40 2009 +0100
     3.3 @@ -2246,13 +2246,13 @@
     3.4    by simp
     3.5  
     3.6  code_modulename SML
     3.7 -  Int Integer
     3.8 +  Int Arith
     3.9  
    3.10  code_modulename OCaml
    3.11 -  Int Integer
    3.12 +  Int Arith
    3.13  
    3.14  code_modulename Haskell
    3.15 -  Int Integer
    3.16 +  Int Arith
    3.17  
    3.18  types_code
    3.19    "int" ("int")

     4.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 30 14:02:42 2009 +0100
     4.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 30 18:32:40 2009 +0100
     4.3 @@ -424,22 +424,13 @@
     4.4  text {* Module names *}
     4.5  
     4.6  code_modulename SML
     4.7 -  Nat Integer
     4.8 -  Divides Integer
     4.9 -  Ring_and_Field Integer
    4.10 -  Efficient_Nat Integer
    4.11 +  Efficient_Nat Arith
    4.12  
    4.13  code_modulename OCaml
    4.14 -  Nat Integer
    4.15 -  Divides Integer
    4.16 -  Ring_and_Field Integer
    4.17 -  Efficient_Nat Integer
    4.18 +  Efficient_Nat Arith
    4.19  
    4.20  code_modulename Haskell
    4.21 -  Nat Integer
    4.22 -  Divides Integer
    4.23 -  Ring_and_Field Integer
    4.24 -  Efficient_Nat Integer
    4.25 +  Efficient_Nat Arith
    4.26  
    4.27  hide const int
    4.28  

     5.1 --- a/src/HOL/Nat.thy	Fri Oct 30 14:02:42 2009 +0100
     5.2 +++ b/src/HOL/Nat.thy	Fri Oct 30 18:32:40 2009 +0100
     5.3 @@ -1674,4 +1674,16 @@
     5.4  class size =
     5.5    fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
     5.6  
     5.7 +
     5.8 +subsection {* code module namespace *}
     5.9 +
    5.10 +code_modulename SML
    5.11 +  Nat Arith
    5.12 +
    5.13 +code_modulename OCaml
    5.14 +  Nat Arith
    5.15 +
    5.16 +code_modulename Haskell
    5.17 +  Nat Arith
    5.18 +
    5.19  end

     6.1 --- a/src/HOL/OrderedGroup.thy	Fri Oct 30 14:02:42 2009 +0100
     6.2 +++ b/src/HOL/OrderedGroup.thy	Fri Oct 30 18:32:40 2009 +0100
     6.3 @@ -1409,4 +1409,13 @@
     6.4    Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
     6.5  *}
     6.6  
     6.7 +code_modulename SML
     6.8 +  OrderedGroup Arith
     6.9 +
    6.10 +code_modulename OCaml
    6.11 +  OrderedGroup Arith
    6.12 +
    6.13 +code_modulename Haskell
    6.14 +  OrderedGroup Arith
    6.15 +
    6.16  end

     7.1 --- a/src/HOL/Power.thy	Fri Oct 30 14:02:42 2009 +0100
     7.2 +++ b/src/HOL/Power.thy	Fri Oct 30 18:32:40 2009 +0100
     7.3 @@ -467,4 +467,13 @@
     7.4  
     7.5  declare power.power.simps [code]
     7.6  
     7.7 +code_modulename SML
     7.8 +  Power Arith
     7.9 +
    7.10 +code_modulename OCaml
    7.11 +  Power Arith
    7.12 +
    7.13 +code_modulename Haskell
    7.14 +  Power Arith
    7.15 +
    7.16  end

     8.1 --- a/src/HOL/Ring_and_Field.thy	Fri Oct 30 14:02:42 2009 +0100
     8.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Oct 30 18:32:40 2009 +0100
     8.3 @@ -2374,4 +2374,14 @@
     8.4    then show ?thesis by simp
     8.5  qed
     8.6  
     8.7 +
     8.8 +code_modulename SML
     8.9 +  Ring_and_Field Arith
    8.10 +
    8.11 +code_modulename OCaml
    8.12 +  Ring_and_Field Arith
    8.13 +
    8.14 +code_modulename Haskell
    8.15 +  Ring_and_Field Arith
    8.16 +
    8.17  end