| changeset 41022 | 81d337539d57 |
| parent 40892 | 6f7292b94652 |
| child 41024 | ba961a606c67 |
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Dec 06 17:33:25 2010 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Mon Dec 06 19:18:02 2010 +0100 @@ -10,7 +10,6 @@ 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)"]] -declare [[coercion int]] declare [[coercion "% x . Float x 0"]] declare [[coercion "real::float\<Rightarrow>real"]]