src/HOL/Library/Code_Char_chr.thy
changeset 49446 6efff142bb54
parent 39535 d7728f65b353
child 52280 0a2371e7ced3
     1.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Jul 23 09:26:55 2012 +0200
     1.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Mon Jul 23 09:28:03 2012 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  code_const int_of_char and char_of_int
     1.5    (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
     1.6    (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
     1.7 -  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
     1.8 +  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
     1.9    (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    1.10  
    1.11  end