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 37223 5226259b6fa2
parent 37050 4a021f6be77c
child 37388 793618618f78 
--- 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