src/HOL/Library/Efficient_Nat.thy
changeset 38771 f9cd27cbe8a4
parent 37969 3bf1fffcdd48
child 38774 567b94f8bb6e
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Aug 25 22:47:04 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 10:16:22 2010 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4  
     1.5  code_type nat
     1.6    (Haskell "Nat.Nat")
     1.7 -  (Scala "Nat")
     1.8 +  (Scala "Nat.Nat")
     1.9  
    1.10  code_instance nat :: eq
    1.11    (Haskell -)
    1.12 @@ -397,7 +397,7 @@
    1.13  
    1.14  code_const int and nat
    1.15    (Haskell "toInteger" and "fromInteger")
    1.16 -  (Scala "!_.as'_BigInt" and "Nat")
    1.17 +  (Scala "!_.as'_BigInt" and "Nat.Nat")
    1.18  
    1.19  text {* Conversion from and to code numerals. *}
    1.20  
    1.21 @@ -405,14 +405,14 @@
    1.22    (SML "IntInf.toInt")
    1.23    (OCaml "_")
    1.24    (Haskell "!(fromInteger/ ./ toInteger)")
    1.25 -  (Scala "!Natural(_.as'_BigInt)")
    1.26 +  (Scala "!Natural.Nat(_.as'_BigInt)")
    1.27    (Eval "_")
    1.28  
    1.29  code_const Code_Numeral.nat_of
    1.30    (SML "IntInf.fromInt")
    1.31    (OCaml "_")
    1.32    (Haskell "!(fromInteger/ ./ toInteger)")
    1.33 -  (Scala "!Nat(_.as'_BigInt)")
    1.34 +  (Scala "!Nat.Nat(_.as'_BigInt)")
    1.35    (Eval "_")
    1.36  
    1.37  text {* Using target language arithmetic operations whenever appropriate *}