--- a/src/HOL/Library/Efficient_Nat.thy Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Aug 26 10:16:22 2010 +0200
@@ -330,7 +330,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat")
+ (Scala "Nat.Nat")
code_instance nat :: eq
(Haskell -)
@@ -397,7 +397,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "Nat")
+ (Scala "!_.as'_BigInt" and "Nat.Nat")
text {* Conversion from and to code numerals. *}
@@ -405,14 +405,14 @@
(SML "IntInf.toInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Natural(_.as'_BigInt)")
+ (Scala "!Natural.Nat(_.as'_BigInt)")
(Eval "_")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Nat(_.as'_BigInt)")
+ (Scala "!Nat.Nat(_.as'_BigInt)")
(Eval "_")
text {* Using target language arithmetic operations whenever appropriate *}