src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 60017 b785d6d06430
parent 54489 03ff4d1e6784
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4    constant ln \<rightharpoonup>
     1.5      (SML) "Math.ln"
     1.6      and (OCaml) "Pervasives.ln"
     1.7 -declare ln_def[code del]
     1.8 +declare ln_real_def[code del]
     1.9  
    1.10  code_printing
    1.11    constant cos \<rightharpoonup>