# HG changeset patch
# User haftmann
# Date 1282817990 -7200
# Node ID 567b94f8bb6e5aed1f1387abdbe5ef85e483d940
# Parent  f9837065b5e88dbd6bbcf7fea62b5b81f78d4444
tuned includes

diff -r f9837065b5e8 -r 567b94f8bb6e src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Thu Aug 26 12:19:49 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Thu Aug 26 12:19:50 2010 +0200
@@ -9,9 +9,7 @@
 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
 
 code_include Haskell "Natural"
-{*import Data.Array.ST;
-
-newtype Natural = Natural Integer deriving (Eq, Show, Read);
+{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
 
 instance Num Natural where {
   fromInteger k = Natural (if k >= 0 then k else 0);
@@ -54,8 +52,8 @@
 
 code_reserved Haskell Natural
 
-code_include Scala "Natural" {*
-import scala.Math
+code_include Scala "Natural"
+{*import scala.Math
 
 object Nat {
 
diff -r f9837065b5e8 -r 567b94f8bb6e src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 12:19:49 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 12:19:50 2010 +0200
@@ -242,8 +242,8 @@
   and @{typ int}.
 *}
 
-code_include Haskell "Nat" {*
-newtype Nat = Nat Integer deriving (Eq, Show, Read);
+code_include Haskell "Nat"
+{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
 
 instance Num Nat where {
   fromInteger k = Nat (if k >= 0 then k else 0);
@@ -280,8 +280,8 @@
 
 code_reserved Haskell Nat
 
-code_include Scala "Nat" {*
-import scala.Math
+code_include Scala "Nat"
+{*import scala.Math
 
 object Nat {