src/HOL/Library/Code_Target_Nat.thy
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 53027 1774d569b604
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -123,14 +123,9 @@
     1.4    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
     1.5    by transfer auto
     1.6  
     1.7 -code_modulename SML
     1.8 -  Code_Target_Nat Arith
     1.9 -
    1.10 -code_modulename OCaml
    1.11 -  Code_Target_Nat Arith
    1.12 -
    1.13 -code_modulename Haskell
    1.14 -  Code_Target_Nat Arith
    1.15 +code_identifier
    1.16 +  code_module Code_Target_Nat \<rightharpoonup>
    1.17 +    (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.18  
    1.19  end
    1.20