src/HOL/RealDef.thy
changeset 41024 ba961a606c67
parent 41022 81d337539d57
child 41231 2e901158675e
equal deleted inserted replaced
41023:9118eb4eb8dc 41024:ba961a606c67
  1112 declare [[coercion_enabled]]
  1112 declare [[coercion_enabled]]
  1113 declare [[coercion "real::nat\<Rightarrow>real"]]
  1113 declare [[coercion "real::nat\<Rightarrow>real"]]
  1114 declare [[coercion "real::int\<Rightarrow>real"]]
  1114 declare [[coercion "real::int\<Rightarrow>real"]]
  1115 declare [[coercion "int"]]
  1115 declare [[coercion "int"]]
  1116 
  1116 
       
  1117 declare [[coercion_map map]]
       
  1118 declare [[coercion_map "% f g h . g o h o f"]]
       
  1119 declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
       
  1120 
  1117 lemma real_eq_of_nat: "real = of_nat"
  1121 lemma real_eq_of_nat: "real = of_nat"
  1118   unfolding real_of_nat_def ..
  1122   unfolding real_of_nat_def ..
  1119 
  1123 
  1120 lemma real_eq_of_int: "real = of_int"
  1124 lemma real_eq_of_int: "real = of_int"
  1121   unfolding real_of_int_def ..
  1125   unfolding real_of_int_def ..