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