# HG changeset patch
# User haftmann
# Date 1275381053 -7200
# Node ID 5226259b6fa24114a3a09e4e6785471b95ab1c46
# Parent  4d984bc33c6681a34ac2a414c4c850128bf86ff0
corrected implementation

diff -r 4d984bc33c66 -r 5226259b6fa2 src/HOL/Library/Efficient_Nat.thy
--- 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)