uniform module names for code generation
authorhaftmann
Sat May 19 11:33:21 2007 +0200 (2007-05-19)
changeset 2301700c0e4c42396
parent 23016 fd7cd1edc18d
child 23018 1d29bc31b0cb
uniform module names for code generation
src/HOL/Divides.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/Executable_Real.thy
     1.1 --- a/src/HOL/Divides.thy	Sat May 19 11:33:20 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat May 19 11:33:21 2007 +0200
     1.3 @@ -929,10 +929,13 @@
     1.4    by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
     1.5  
     1.6  code_modulename SML
     1.7 -  Divides Integer
     1.8 +  Divides Nat
     1.9  
    1.10  code_modulename OCaml
    1.11 -  Divides Integer
    1.12 +  Divides Nat
    1.13 +
    1.14 +code_modulename Haskell
    1.15 +  Divides Nat
    1.16  
    1.17  hide (open) const divmod dvd_nat
    1.18  
     2.1 --- a/src/HOL/Library/EfficientNat.thy	Sat May 19 11:33:20 2007 +0200
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Sat May 19 11:33:21 2007 +0200
     2.3 @@ -388,6 +388,10 @@
     2.4    Nat Integer
     2.5    EfficientNat Integer
     2.6  
     2.7 +code_modulename Haskell
     2.8 +  Nat Integer
     2.9 +  EfficientNat Integer
    2.10 +
    2.11  hide const nat_of_int
    2.12  
    2.13  end
     3.1 --- a/src/HOL/Library/Executable_Real.thy	Sat May 19 11:33:20 2007 +0200
     3.2 +++ b/src/HOL/Library/Executable_Real.thy	Sat May 19 11:33:21 2007 +0200
     3.3 @@ -467,6 +467,18 @@
     3.4    "number_of k = real_int (number_of k)"
     3.5    by (simp add: real_int_def)
     3.6  
     3.7 +code_modulename SML
     3.8 +  RealDef Real
     3.9 +  Executable_Real Real
    3.10 +
    3.11 +code_modulename OCaml
    3.12 +  RealDef Real
    3.13 +  Executable_Real Real
    3.14 +
    3.15 +code_modulename Haskell
    3.16 +  RealDef Real
    3.17 +  Executable_Real Real
    3.18 +
    3.19  types_code real ("{* int * int *}")
    3.20  attach (term_of) {*
    3.21  fun term_of_real (p, q) =