src/HOL/Nat.thy
changeset 33364 2bd12592c5e8
parent 33274 b6ff7db522b5
child 33657 a4179bf442d1
--- 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