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.
Change coercion for RealDef to use function application (not composition)
authornoschinl
Fri, 25 Mar 2011 15:22:09 +0100
changeset 42112 9cb122742f5c
parent 42111 d1c761375a75
child 42113 3c71630041c7
child 42117 306713ec55c3
Change coercion for RealDef to use function application (not composition)
src/HOL/RealDef.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/RealDef.thy	Fri Mar 25 11:19:01 2011 +0100
+++ b/src/HOL/RealDef.thy	Fri Mar 25 15:22:09 2011 +0100
@@ -1115,7 +1115,7 @@
 declare [[coercion "int"]]
 
 declare [[coercion_map map]]
-declare [[coercion_map "% f g h . g o h o f"]]
+declare [[coercion_map "% f g h x. g (h (f x))"]]
 declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
 
 lemma real_eq_of_nat: "real = of_nat"
isabelle