src/HOL/Library/Float.thy
changeset 51375 d9e62d9c98de
parent 49834 b27bbb021df1
child 51542 738598beeb26
     1.1 --- a/src/HOL/Library/Float.thy	Fri Mar 08 13:14:23 2013 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Fri Mar 08 13:21:06 2013 +0100
     1.3 @@ -223,15 +223,15 @@
     1.4    done
     1.5  
     1.6  lemma transfer_numeral [transfer_rule]: 
     1.7 -  "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
     1.8 -  unfolding fun_rel_def cr_float_def by simp
     1.9 +  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
    1.10 +  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
    1.11  
    1.12  lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
    1.13    by (simp add: minus_numeral[symmetric] del: minus_numeral)
    1.14  
    1.15  lemma transfer_neg_numeral [transfer_rule]: 
    1.16 -  "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    1.17 -  unfolding fun_rel_def cr_float_def by simp
    1.18 +  "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    1.19 +  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
    1.20  
    1.21  lemma
    1.22    shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"