1.1 --- a/src/HOL/Library/Code_Natural.thy	Wed Aug 25 22:47:04 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Thu Aug 26 10:16:22 2010 +0200
     1.3 @@ -57,45 +57,45 @@
     1.4  code_include Scala "Natural" {*
     1.5  import scala.Math
     1.6  
     1.7 -object Natural {
     1.8 +object Nat {
     1.9  
    1.10 -  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    1.11 -  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    1.12 -  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    1.13 +  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    1.14 +  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    1.15 +  def apply(numeral: String): Nat = Nat(BigInt(numeral))
    1.16  
    1.17  }
    1.18  
    1.19 -class Natural private(private val value: BigInt) {
    1.20 +class Nat private(private val value: BigInt) {
    1.21  
    1.22    override def hashCode(): Int = this.value.hashCode()
    1.23  
    1.24    override def equals(that: Any): Boolean = that match {
    1.25 -    case that: Natural => this equals that
    1.26 +    case that: Nat => this equals that
    1.27      case _ => false
    1.28    }
    1.29  
    1.30    override def toString(): String = this.value.toString
    1.31  
    1.32 -  def equals(that: Natural): Boolean = this.value == that.value
    1.33 +  def equals(that: Nat): Boolean = this.value == that.value
    1.34  
    1.35    def as_BigInt: BigInt = this.value
    1.36    def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    1.37        this.value.intValue
    1.38      else error("Int value out of range: " + this.value.toString)
    1.39  
    1.40 -  def +(that: Natural): Natural = new Natural(this.value + that.value)
    1.41 -  def -(that: Natural): Natural = Natural(this.value - that.value)
    1.42 -  def *(that: Natural): Natural = new Natural(this.value * that.value)
    1.43 +  def +(that: Nat): Nat = new Nat(this.value + that.value)
    1.44 +  def -(that: Nat): Nat = Nat(this.value - that.value)
    1.45 +  def *(that: Nat): Nat = new Nat(this.value * that.value)
    1.46  
    1.47 -  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    1.48 +  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
    1.49      else {
    1.50        val (k, l) = this.value /% that.value
    1.51 -      (new Natural(k), new Natural(l))
    1.52 +      (new Nat(k), new Nat(l))
    1.53      }
    1.54  
    1.55 -  def <=(that: Natural): Boolean = this.value <= that.value
    1.56 +  def <=(that: Nat): Boolean = this.value <= that.value
    1.57  
    1.58 -  def <(that: Natural): Boolean = this.value < that.value
    1.59 +  def <(that: Nat): Boolean = this.value < that.value
    1.60  
    1.61  }
    1.62  *}
    1.63 @@ -104,7 +104,7 @@
    1.64  
    1.65  code_type code_numeral
    1.66    (Haskell "Natural.Natural")
    1.67 -  (Scala "Natural")
    1.68 +  (Scala "Natural.Nat")
    1.69  
    1.70  setup {*
    1.71    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}