Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Backed out changeset: 3fe7242f8346,
authortraytel
Fri, 15 Feb 2013 16:17:05 +0100
changeset 51163 4e53be4ad845
parent 51162 310b94ed1815
child 51164 eba05aaa8612
Backed out changeset: 3fe7242f8346, many proofs (e.g. in Extended_Real and Approximation) rely on coercions not being lifted over sets
src/HOL/RealDef.thy file | annotate | diff | comparison | revisions 
--- 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)"]]
isabelle