# HG changeset patch
# User traytel
# Date 1360941425 -3600
# Node ID 4e53be4ad84536dc1a6c6b9038b29672dc757288
# Parent  310b94ed1815f42c728c5cae2742b355fbb41dd1
Backed out changeset: 3fe7242f8346,
many proofs (e.g. in Extended_Real and Approximation) rely on coercions not being lifted over sets

diff -r 310b94ed1815 -r 4e53be4ad845 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Feb 15 12:48:20 2013 +0100
+++ b/src/HOL/RealDef.thy	Fri Feb 15 16:17:05 2013 +0100
@@ -987,7 +987,6 @@
 declare [[coercion "int"]]
 
 declare [[coercion_map map]]
-declare [[coercion_map image]]
 declare [[coercion_map "% f g h x. g (h (f x))"]]
 declare [[coercion_map "% f g (x,y) . (f x, g y)"]]