src/HOL/Imperative_HOL/Array.thy
changeset 69906 55534affe445
parent 66003 5b2fab45db92
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -458,13 +458,13 @@
     1.4  
     1.5  code_printing type_constructor array \<rightharpoonup> (OCaml) "_/ array"
     1.6  code_printing constant Array \<rightharpoonup> (OCaml) "failwith/ \"bare Array\""
     1.7 -code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)"
     1.8 +code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Z.to'_int/ _)/ _)"
     1.9  code_printing constant Array.of_list \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)"
    1.10  code_printing constant Array.make' \<rightharpoonup> (OCaml)
    1.11 -  "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))"
    1.12 -code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))"
    1.13 -code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))"
    1.14 -code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)"
    1.15 +  "(fun/ ()/ ->/ Array.init/ (Z.to'_int/ _)/ (fun k'_ ->/ _/ (Z.of'_int/ k'_)))"
    1.16 +code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Z.of'_int/ (Array.length/ _))"
    1.17 +code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Z.to'_int/ _))"
    1.18 +code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Z.to'_int/ _)/ _)"
    1.19  code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
    1.20  
    1.21  code_reserved OCaml Array