# HG changeset patch
# User haftmann
# Date 1497956865 -7200
# Node ID 9225370db5f035b22715b24bae2b8d2bce850c27
# Parent  fd3e128b174f33360b84a6239a5ecd66cdb2d71e
obsolete

diff -r fd3e128b174f -r 9225370db5f0 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Jun 20 13:07:44 2017 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Jun 20 13:07:45 2017 +0200
@@ -33,13 +33,11 @@
   constant "0 :: real" \<rightharpoonup>
     (SML) "0.0"
     and (OCaml) "0.0"
-declare zero_real_code[code_unfold del]
 
 code_printing
   constant "1 :: real" \<rightharpoonup>
     (SML) "1.0"
     and (OCaml) "1.0"
-declare one_real_code[code_unfold del]
 
 code_printing
   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>