move coercions to appropriate places
authorhoelzl
Mon Dec 06 19:54:48 2010 +0100 (2010-12-06)
changeset 41024ba961a606c67
parent 41023 9118eb4eb8dc
child 41025 8b2cd85ecf11
move coercions to appropriate places
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Float.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Dec 03 15:25:14 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 06 19:54:48 2010 +0100
     1.3 @@ -7,12 +7,6 @@
     1.4  imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
     1.5  begin
     1.6  
     1.7 -declare [[coercion_map map]]
     1.8 -declare [[coercion_map "% f g h . g o h o f"]]
     1.9 -declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
    1.10 -declare [[coercion "% x . Float x 0"]]
    1.11 -declare [[coercion "real::float\<Rightarrow>real"]]
    1.12 -
    1.13  section "Horner Scheme"
    1.14  
    1.15  subsection {* Define auxiliary helper @{text horner} function *}
     2.1 --- a/src/HOL/Library/Float.thy	Fri Dec 03 15:25:14 2010 +0100
     2.2 +++ b/src/HOL/Library/Float.thy	Mon Dec 06 19:54:48 2010 +0100
     2.3 @@ -21,6 +21,9 @@
     2.4  defs (overloaded)
     2.5    real_of_float_def [code_unfold]: "real == of_float"
     2.6  
     2.7 +declare [[coercion "% x . Float x 0"]]
     2.8 +declare [[coercion "real::float\<Rightarrow>real"]]
     2.9 +
    2.10  primrec mantissa :: "float \<Rightarrow> int" where
    2.11    "mantissa (Float a b) = a"
    2.12  
     3.1 --- a/src/HOL/RealDef.thy	Fri Dec 03 15:25:14 2010 +0100
     3.2 +++ b/src/HOL/RealDef.thy	Mon Dec 06 19:54:48 2010 +0100
     3.3 @@ -1114,6 +1114,10 @@
     3.4  declare [[coercion "real::int\<Rightarrow>real"]]
     3.5  declare [[coercion "int"]]
     3.6  
     3.7 +declare [[coercion_map map]]
     3.8 +declare [[coercion_map "% f g h . g o h o f"]]
     3.9 +declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
    3.10 +
    3.11  lemma real_eq_of_nat: "real = of_nat"
    3.12    unfolding real_of_nat_def ..
    3.13