src/HOL/Library/Efficient_Nat.thy
changeset 49446 6efff142bb54
parent 49088 1b609a7837ef
child 49583 084cd758a8ab
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 23 09:26:55 2012 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 23 09:28:03 2012 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4  text {* For Haskell and Scala, things are slightly different again. *}
     1.5  
     1.6  code_const int and nat
     1.7 -  (Haskell "toInteger" and "fromInteger")
     1.8 +  (Haskell "Prelude.toInteger" and "Prelude.fromInteger")
     1.9    (Scala "!_.as'_BigInt" and "Nat")
    1.10  
    1.11  text {* Alternativ implementation for @{const of_nat} *}
    1.12 @@ -189,14 +189,14 @@
    1.13  code_const Code_Numeral.of_nat
    1.14    (SML "IntInf.toInt")
    1.15    (OCaml "_")
    1.16 -  (Haskell "!(fromInteger/ ./ toInteger)")
    1.17 +  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
    1.18    (Scala "!Natural(_.as'_BigInt)")
    1.19    (Eval "_")
    1.20  
    1.21  code_const Code_Numeral.nat_of
    1.22    (SML "IntInf.fromInt")
    1.23    (OCaml "_")
    1.24 -  (Haskell "!(fromInteger/ ./ toInteger)")
    1.25 +  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
    1.26    (Scala "!Nat(_.as'_BigInt)")
    1.27    (Eval "_")
    1.28