proper theory name (cf. e84f82418e09);
authorwenzelm
Thu Dec 02 21:23:56 2010 +0100 (2010-12-02)
changeset 408926f7292b94652
parent 40891 74877f1f3c68
child 40893 7d88ebdce380
child 40897 1eb1b2f9d062
proper theory name (cf. e84f82418e09);
src/HOL/Decision_Procs/Approximation.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 02 21:04:20 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 02 21:23:56 2010 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  
     1.5  header {* Prove Real Valued Inequalities by Computation *}
     1.6  
     1.7 -theory Approximation_coercion
     1.8 +theory Approximation
     1.9  imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
    1.10  begin
    1.11