# HG changeset patch # User haftmann # Date 1282821914 -7200 # Node ID 741ca0c98f6f0b42df172bd826ed653a303f2c68 # Parent 567b94f8bb6e5aed1f1387abdbe5ef85e483d940 re-added accidental omission diff -r 567b94f8bb6e -r 741ca0c98f6f src/HOL/Library/Code_Natural.thy --- a/src/HOL/Library/Code_Natural.thy Thu Aug 26 12:19:50 2010 +0200 +++ b/src/HOL/Library/Code_Natural.thy Thu Aug 26 13:25:14 2010 +0200 @@ -9,7 +9,9 @@ section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *} code_include Haskell "Natural" -{*newtype Natural = Natural Integer deriving (Eq, Show, Read); +{*import Data.Array.ST; + +newtype Natural = Natural Integer deriving (Eq, Show, Read); instance Num Natural where { fromInteger k = Natural (if k >= 0 then k else 0);