# HG changeset patch
# User nipkow
# Date 1563444402 -7200
# Node ID 04f492d004fab6a6e83dd014d82d42b0f6bc02f8
# Parent  af25255bda02ddbf524dffb0cd2bf41e0042964e
added forgotten declaration provided by Florian Haftmann

diff -r af25255bda02 -r 04f492d004fa src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Wed Jul 17 22:24:20 2019 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Thu Jul 18 12:06:42 2019 +0200
@@ -199,7 +199,9 @@
   "uminus :: real \<Rightarrow> real"
   "minus :: real \<Rightarrow> real \<Rightarrow> real"
   "times :: real \<Rightarrow> real \<Rightarrow> real"
-  "divide :: real \<Rightarrow> real \<Rightarrow> real"]]
+  "divide :: real \<Rightarrow> real \<Rightarrow> real"
+  "(<) :: real \<Rightarrow> real \<Rightarrow> bool"
+  "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"]]
 
 lemma [code]: "inverse r = 1 / r" for r :: real
   by (fact inverse_eq_divide)