tuned includes
authorhaftmann
Thu Aug 26 12:19:50 2010 +0200 (2010-08-26 ago)
changeset 38774567b94f8bb6e
parent 38773 f9837065b5e8
child 38775 741ca0c98f6f
child 38777 a94559e26000
tuned includes
src/HOL/Library/Code_Natural.thy
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Natural.thy	Thu Aug 26 12:19:49 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Thu Aug 26 12:19:50 2010 +0200
     1.3 @@ -9,9 +9,7 @@
     1.4  section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
     1.5  
     1.6  code_include Haskell "Natural"
     1.7 -{*import Data.Array.ST;
     1.8 -
     1.9 -newtype Natural = Natural Integer deriving (Eq, Show, Read);
    1.10 +{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
    1.11  
    1.12  instance Num Natural where {
    1.13    fromInteger k = Natural (if k >= 0 then k else 0);
    1.14 @@ -54,8 +52,8 @@
    1.15  
    1.16  code_reserved Haskell Natural
    1.17  
    1.18 -code_include Scala "Natural" {*
    1.19 -import scala.Math
    1.20 +code_include Scala "Natural"
    1.21 +{*import scala.Math
    1.22  
    1.23  object Nat {
    1.24  
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 12:19:49 2010 +0200
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 12:19:50 2010 +0200
     2.3 @@ -242,8 +242,8 @@
     2.4    and @{typ int}.
     2.5  *}
     2.6  
     2.7 -code_include Haskell "Nat" {*
     2.8 -newtype Nat = Nat Integer deriving (Eq, Show, Read);
     2.9 +code_include Haskell "Nat"
    2.10 +{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
    2.11  
    2.12  instance Num Nat where {
    2.13    fromInteger k = Nat (if k >= 0 then k else 0);
    2.14 @@ -280,8 +280,8 @@
    2.15  
    2.16  code_reserved Haskell Nat
    2.17  
    2.18 -code_include Scala "Nat" {*
    2.19 -import scala.Math
    2.20 +code_include Scala "Nat"
    2.21 +{*import scala.Math
    2.22  
    2.23  object Nat {
    2.24