# 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\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\real"]] + primrec mantissa :: "float \ 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\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 ..