Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Efficient_Nat.thy
changeset 37846 6f8b1bb4d248
parent 37388 793618618f78
child 37878 d016aaead7a2 
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 16 15:28:22 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 16 15:28:23 2010 +0200
@@ -312,9 +312,9 @@
   def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
-  def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
+  def as_Int: Int = if (this.value >= Math.MIN_INT && this.value <= Math.MAX_INT)
       this.value.intValue
-    else error("Int value too big:" + this.value.toString)
+    else this.value.intValue
 
   def +(that: Nat): Nat = new Nat(this.value + that.value)
   def -(that: Nat): Nat = Nat(this.value - that.value)
isabelle