src/HOL/Decision_Procs/Approximation.thy
changeset 30122 1c912a9d8200
parent 29823 0ab754d13ccd
child 30273 ecd6f0ca62ea
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:55:47 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:56:59 2009 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4 -(* Title:     HOL/Reflection/Approximation.thy
     1.5 - * Author:    Johannes Hölzl <hoelzl@in.tum.de> 2008 / 2009
     1.6 - *)
     1.7 +(*  Title:      HOL/Reflection/Approximation.thy
     1.8 +    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
     1.9 +*)
    1.10 +
    1.11  header {* Prove unequations about real numbers by computation *}
    1.12 +
    1.13  theory Approximation
    1.14  imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
    1.15  begin