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.
obsolete
authorhaftmann
Tue, 20 Jun 2017 13:07:45 +0200
changeset 66147 9225370db5f0
parent 66146 fd3e128b174f
child 66148 5e60c2d0a1f1
obsolete
src/HOL/Library/Code_Real_Approx_By_Float.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle