Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected implementation
authorhaftmann
Tue, 01 Jun 2010 10:30:53 +0200
changeset 37223 5226259b6fa2
parent 37222 4d984bc33c66
child 37224 f4d3c929c526
corrected implementation
src/HOL/Library/Efficient_Nat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 10:30:53 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 10:30:53 2010 +0200
@@ -317,7 +317,7 @@
     else error("Int value too big:" + this.value.toString)
 
   def +(that: Nat): Nat = new Nat(this.value + that.value)
-  def -(that: Nat): Nat = Nat(this.value + that.value)
+  def -(that: Nat): Nat = Nat(this.value - that.value)
   def *(that: Nat): Nat = new Nat(this.value * that.value)
 
   def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
isabelle