corrected implementation
authorhaftmann
Tue Jun 01 10:30:53 2010 +0200 (2010-06-01)
changeset 372235226259b6fa2
parent 37222 4d984bc33c66
child 37224 f4d3c929c526
corrected implementation
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 10:30:53 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 10:30:53 2010 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4      else error("Int value too big:" + this.value.toString)
     1.5  
     1.6    def +(that: Nat): Nat = new Nat(this.value + that.value)
     1.7 -  def -(that: Nat): Nat = Nat(this.value + that.value)
     1.8 +  def -(that: Nat): Nat = Nat(this.value - that.value)
     1.9    def *(that: Nat): Nat = new Nat(this.value * that.value)
    1.10  
    1.11    def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)