src/HOL/Library/Float.thy
changeset 55945 e96383acecf9
parent 55565 f663fc1e653b
child 56410 a14831ac3023
     1.1 --- a/src/HOL/Library/Float.thy	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Mar 06 15:40:33 2014 +0100
     1.3 @@ -223,15 +223,15 @@
     1.4    done
     1.5  
     1.6  lemma transfer_numeral [transfer_rule]:
     1.7 -  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
     1.8 -  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
     1.9 +  "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
    1.10 +  unfolding rel_fun_def float.pcr_cr_eq  cr_float_def by simp
    1.11  
    1.12  lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
    1.13    by simp
    1.14  
    1.15  lemma transfer_neg_numeral [transfer_rule]:
    1.16 -  "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
    1.17 -  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
    1.18 +  "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
    1.19 +  unfolding rel_fun_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)"