--- a/src/HOL/Decision_Procs/Approximation.thy Fri Dec 03 15:25:14 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Dec 06 19:54:48 2010 +0100
@@ -7,12 +7,6 @@
imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
begin
-declare [[coercion_map map]]
-declare [[coercion_map "% f g h . g o h o f"]]
-declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
-declare [[coercion "% x . Float x 0"]]
-declare [[coercion "real::float\<Rightarrow>real"]]
-
section "Horner Scheme"
subsection {* Define auxiliary helper @{text horner} function *}