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