src/HOL/Library/Efficient_Nat.thy
changeset 37878 d016aaead7a2
parent 37846 6f8b1bb4d248
child 37892 3d8857f42a64
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 19 11:55:42 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 19 11:55:42 2010 +0200
     1.3 @@ -337,7 +337,7 @@
     1.4  
     1.5  code_type nat
     1.6    (Haskell "Nat.Nat")
     1.7 -  (Scala "Nat.Nat")
     1.8 +  (Scala "Nat")
     1.9  
    1.10  code_instance nat :: eq
    1.11    (Haskell -)
    1.12 @@ -405,7 +405,7 @@
    1.13  
    1.14  code_const int and nat
    1.15    (Haskell "toInteger" and "fromInteger")
    1.16 -  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
    1.17 +  (Scala "!_.as'_BigInt" and "Nat")
    1.18  
    1.19  text {* Conversion from and to indices. *}
    1.20  
    1.21 @@ -419,7 +419,7 @@
    1.22    (SML "IntInf.fromInt")
    1.23    (OCaml "_")
    1.24    (Haskell "toEnum")
    1.25 -  (Scala "!Nat.Nat((_))")
    1.26 +  (Scala "Nat")
    1.27  
    1.28  text {* Using target language arithmetic operations whenever appropriate *}
    1.29