src/HOL/Semiring_Normalization.thy
changeset 52435 6646bb548c6b
parent 48891 c0eafbd55de3
child 53076 47c9aff07725
--- a/src/HOL/Semiring_Normalization.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Semiring_Normalization.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -219,13 +219,7 @@
 
 hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
 
-code_modulename SML
-  Semiring_Normalization Arith
-
-code_modulename OCaml
-  Semiring_Normalization Arith
-
-code_modulename Haskell
-  Semiring_Normalization Arith
+code_identifier
+  code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end