| changeset 42112 | 9cb122742f5c |
| parent 41920 | d4fb7a418152 |
| child 42311 | eb32a8474a57 |
--- 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"