| changeset 41024 | ba961a606c67 |
| parent 41022 | 81d337539d57 |
| child 41231 | 2e901158675e |
--- a/src/HOL/RealDef.thy Fri Dec 03 15:25:14 2010 +0100 +++ b/src/HOL/RealDef.thy Mon Dec 06 19:54:48 2010 +0100 @@ -1114,6 +1114,10 @@ declare [[coercion "real::int\<Rightarrow>real"]] declare [[coercion "int"]] +declare [[coercion_map map]] +declare [[coercion_map "% f g h . g o h o f"]] +declare [[coercion_map "% f g (x,y) . (f x, g y)"]] + lemma real_eq_of_nat: "real = of_nat" unfolding real_of_nat_def ..