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.
coercions between base types can be lifted to sets
authortraytel
Fri, 15 Feb 2013 15:22:16 +0100
changeset 51159 3fe7242f8346
parent 51158 f432363eebf4
child 51160 599ff65b85e2
coercions between base types can be lifted to sets
src/HOL/RealDef.thy file | annotate | diff | comparison | revisions 
--- 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)"]]
isabelle