# HG changeset patch
# User wenzelm
# Date 1291321436 -3600
# Node ID 6f7292b946520a732ae74d7826de59e1bc8105e9
# Parent  74877f1f3c6888b0a8526a2733d58a849b502726
proper theory name (cf. e84f82418e09);

diff -r 74877f1f3c68 -r 6f7292b94652 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 02 21:04:20 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 02 21:23:56 2010 +0100
@@ -3,7 +3,7 @@
 
 header {* Prove Real Valued Inequalities by Computation *}
 
-theory Approximation_coercion
+theory Approximation
 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
 begin