Mercurial > isabelle

changeset 75713:91cdf474b64d fix-code_real_approx_by_float

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Support 'late use' of Code_Real_Approx_By_Float.
author Achim D. Brucker <adbrucker@0x5f.org>
date Mon, 25 Jul 2022 08:24:21 +0100
parents 048bbe0bf807
children 0422df1c5bf3
files src/HOL/Library/Code_Real_Approx_By_Float.thy
diffstat 1 files changed, 13 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Jul 23 12:19:45 2022 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Jul 25 08:24:21 2022 +0100
@@ -20,6 +20,8 @@
   purposes.
 \<close>
 
+code_reserved SML Real
+
 code_printing
   type_constructor real \<rightharpoonup>
     (SML) "real"
@@ -183,16 +185,22 @@
 code_printing
   constant Ratreal \<rightharpoonup> (SML)
 
-definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
-  where "Realfract p q = of_int p / of_int q"
+definition Realfract :: "real \<Rightarrow> real \<Rightarrow> real"
+  where "Realfract p q = p / q"
+
+definition Realfract' :: "int \<Rightarrow> int \<Rightarrow> real"
+  where "Realfract' p q = Realfract (of_int p) (of_int q)"
+
+
 
 code_datatype Realfract
 
 code_printing
-  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
+  constant Realfract \<rightharpoonup> (SML) "_/ '// _"
+
 
-lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
-  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
+lemma [code]: "Ratreal r = case_prod Realfract' (quotient_of r)"
+  by (cases r) (simp add: Realfract_def Realfract'_def quotient_of_Fract of_rat_rat)
 
 declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
   "plus :: real \<Rightarrow> real \<Rightarrow> real"