--- a/src/HOL/Decision_Procs/Approximation.thy Wed Apr 07 15:46:06 2021 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 08 12:38:18 2021 +0000
@@ -1,11 +1,11 @@
- (* Author: Johannes Hoelzl, TU Muenchen
+(* Author: Johannes Hoelzl, TU Muenchen
Coercions removed by Dmitriy Traytel *)
theory Approximation
imports
Complex_Main
- "HOL-Library.Code_Target_Numeral"
Approximation_Bounds
+ "HOL-Library.Code_Target_Numeral_Float"
keywords "approximate" :: diag
begin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Target_Numeral_Float.thy Thu Apr 08 12:38:18 2021 +0000
@@ -0,0 +1,16 @@
+(* Title: HOL/Library/Code_Target_Numeral_Float.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Preprocessor setup for floats implemented by target language numerals\<close>
+
+theory Code_Target_Numeral_Float
+imports Float Code_Target_Numeral
+begin
+
+lemma numeral_float_computation_unfold [code_computation_unfold]:
+ \<open>numeral k = Float (int_of_integer (Code_Numeral.positive k)) 0\<close>
+ \<open>- numeral k = Float (int_of_integer (Code_Numeral.negative k)) 0\<close>
+ by (simp_all add: Float.compute_float_numeral Float.compute_float_neg_numeral)
+
+end
--- a/src/HOL/ROOT Wed Apr 07 15:46:06 2021 +0000
+++ b/src/HOL/ROOT Thu Apr 08 12:38:18 2021 +0000
@@ -73,6 +73,7 @@
Code_Prolog
Code_Real_Approx_By_Float
Code_Target_Numeral
+ Code_Target_Numeral_Float
DAList
DAList_Multiset
RBT_Mapping