src/HOL/Library/Code_Binary_Nat.thy
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 53069 d165213e3924
--- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -142,14 +142,9 @@
   by (simp_all add: nat_of_num_numeral)
 
 
-code_modulename SML
-  Code_Binary_Nat Arith
-
-code_modulename OCaml
-  Code_Binary_Nat Arith
-
-code_modulename Haskell
-  Code_Binary_Nat Arith
+code_identifier
+  code_module Code_Binary_Nat \<rightharpoonup>
+    (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 hide_const (open) dup sub