# HG changeset patch
# User traytel
# Date 1360938136 -3600
# Node ID 3fe7242f834625614a0701f02816bc2885a2bfc8
# Parent  f432363eebf478c55a2a8b885591635833b96504
coercions between base types can be lifted to sets

diff -r f432363eebf4 -r 3fe7242f8346 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Feb 15 13:54:54 2013 +0100
+++ b/src/HOL/RealDef.thy	Fri Feb 15 15:22:16 2013 +0100
@@ -987,6 +987,7 @@
 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)"]]