# HG changeset patch
# User hoelzl
# Date 1291661688 -3600
# Node ID ba961a606c67763a50099afed96540c2ca6c56c0
# Parent  9118eb4eb8dc4a93b4759f90a308b5364b793a1e
move coercions to appropriate places

diff -r 9118eb4eb8dc -r ba961a606c67 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Dec 03 15:25:14 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 06 19:54:48 2010 +0100
@@ -7,12 +7,6 @@
 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
 begin
 
-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 "% x . Float x 0"]]
-declare [[coercion "real::float\<Rightarrow>real"]]
-
 section "Horner Scheme"
 
 subsection {* Define auxiliary helper @{text horner} function *}
diff -r 9118eb4eb8dc -r ba961a606c67 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Dec 03 15:25:14 2010 +0100
+++ b/src/HOL/Library/Float.thy	Mon Dec 06 19:54:48 2010 +0100
@@ -21,6 +21,9 @@
 defs (overloaded)
   real_of_float_def [code_unfold]: "real == of_float"
 
+declare [[coercion "% x . Float x 0"]]
+declare [[coercion "real::float\<Rightarrow>real"]]
+
 primrec mantissa :: "float \<Rightarrow> int" where
   "mantissa (Float a b) = a"
 
diff -r 9118eb4eb8dc -r ba961a606c67 src/HOL/RealDef.thy
--- 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 ..