src/HOL/Decision_Procs/Approximation.thy
changeset 41024 ba961a606c67
parent 41022 81d337539d57
child 41413 64cd30d6b0b8
equal deleted inserted replaced
41023:9118eb4eb8dc 41024:ba961a606c67
     4 header {* Prove Real Valued Inequalities by Computation *}
     4 header {* Prove Real Valued Inequalities by Computation *}
     5 
     5 
     6 theory Approximation
     6 theory Approximation
     7 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
     7 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
     8 begin
     8 begin
     9 
       
    10 declare [[coercion_map map]]
       
    11 declare [[coercion_map "% f g h . g o h o f"]]
       
    12 declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
       
    13 declare [[coercion "% x . Float x 0"]]
       
    14 declare [[coercion "real::float\<Rightarrow>real"]]
       
    15 
     9 
    16 section "Horner Scheme"
    10 section "Horner Scheme"
    17 
    11 
    18 subsection {* Define auxiliary helper @{text horner} function *}
    12 subsection {* Define auxiliary helper @{text horner} function *}
    19 
    13