tuned code setup

--- 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

--- a/src/HOL/HOL.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/HOL.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -1818,7 +1818,7 @@
 
 code_datatype "TYPE('a\<Colon>{})"
 
-code_datatype Trueprop "prop"
+code_datatype "prop" Trueprop
 
 text {* Code equations *}
 

--- a/src/HOL/Int.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/Int.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -2246,13 +2246,13 @@
   by simp
 
 code_modulename SML
-  Int Integer
+  Int Arith
 
 code_modulename OCaml
-  Int Integer
+  Int Arith
 
 code_modulename Haskell
-  Int Integer
+  Int Arith
 
 types_code
   "int" ("int")

--- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -424,22 +424,13 @@
 text {* Module names *}
 
 code_modulename SML
-  Nat Integer
-  Divides Integer
-  Ring_and_Field Integer
-  Efficient_Nat Integer
+  Efficient_Nat Arith
 
 code_modulename OCaml
-  Nat Integer
-  Divides Integer
-  Ring_and_Field Integer
-  Efficient_Nat Integer
+  Efficient_Nat Arith
 
 code_modulename Haskell
-  Nat Integer
-  Divides Integer
-  Ring_and_Field Integer
-  Efficient_Nat Integer
+  Efficient_Nat Arith
 
 hide const int
 

--- a/src/HOL/Nat.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/Nat.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -1674,4 +1674,16 @@
 class size =
   fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
 
+
+subsection {* code module namespace *}
+
+code_modulename SML
+  Nat Arith
+
+code_modulename OCaml
+  Nat Arith
+
+code_modulename Haskell
+  Nat Arith
+
 end

--- a/src/HOL/OrderedGroup.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -1409,4 +1409,13 @@
   Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
 *}
 
+code_modulename SML
+  OrderedGroup Arith
+
+code_modulename OCaml
+  OrderedGroup Arith
+
+code_modulename Haskell
+  OrderedGroup Arith
+
 end

--- a/src/HOL/Power.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/Power.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -467,4 +467,13 @@
 
 declare power.power.simps [code]
 
+code_modulename SML
+  Power Arith
+
+code_modulename OCaml
+  Power Arith
+
+code_modulename Haskell
+  Power Arith
+
 end

--- a/src/HOL/Ring_and_Field.thy	Fri Oct 30 14:02:42 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Oct 30 18:32:40 2009 +0100
@@ -2374,4 +2374,14 @@
   then show ?thesis by simp
 qed
 
+
+code_modulename SML
+  Ring_and_Field Arith
+
+code_modulename OCaml
+  Ring_and_Field Arith
+
+code_modulename Haskell
+  Ring_and_Field Arith
+
 end