src/HOL/Decision_Procs/Approximation.thy
changeset 30886 dda08b76fa99
parent 30549 d2d7874648bd
child 30952 7ab2716dd93b
equal deleted inserted replaced
30885:a3cfe0e27deb 30886:dda08b76fa99
     1 (* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 *)
     1 (* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 *)
     2 
     2 
     3 header {* Prove unequations about real numbers by computation *}
     3 header {* Prove Real Valued Inequalities by Computation *}
     4 
     4 
     5 theory Approximation
     5 theory Approximation
     6 imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
     6 imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
     7 begin
     7 begin
     8 
     8