| changeset 51163 | 4e53be4ad845 |
| parent 51159 | 3fe7242f8346 |
| child 51185 | 145d76c35f8b |
--- 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)"]]