src/HOL/String.thy
changeset 69906 55534affe445
parent 69879 2731278dfff9
     1.1 --- a/src/HOL/String.thy	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/HOL/String.thy	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -673,7 +673,7 @@
     1.4      (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
     1.5      and (OCaml) "!(let xs = _
     1.6        and chr k =
     1.7 -        let l = Big'_int.int'_of'_big'_int k
     1.8 +        let l = Z.to'_int k
     1.9            in if 0 <= l && l < 128
    1.10            then Char.chr l
    1.11            else failwith \"Non-ASCII character in literal\"
    1.12 @@ -683,7 +683,7 @@
    1.13  | constant String.asciis_of_literal \<rightharpoonup>
    1.14      (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
    1.15      and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
    1.16 -      if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
    1.17 +      if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
    1.18      and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
    1.19      and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
    1.20  | class_instance String.literal :: equal \<rightharpoonup>