Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added forgotten declaration provided by Florian Haftmann
authornipkow
Thu, 18 Jul 2019 12:06:42 +0200
changeset 70377 04f492d004fa
parent 70376 af25255bda02
child 70379 8a7053892d8e
added forgotten declaration provided by Florian Haftmann
src/HOL/Library/Code_Real_Approx_By_Float.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle