src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 69906 55534affe445
parent 69064 5840724b1d71
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -155,7 +155,7 @@
     1.4  code_printing
     1.5    constant real_of_integer \<rightharpoonup>
     1.6      (SML) "Real.fromInt"
     1.7 -    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
     1.8 +    and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
     1.9  
    1.10  context
    1.11  begin