Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Float.thy
changeset 51375 d9e62d9c98de
parent 49834 b27bbb021df1
child 51542 738598beeb26 
--- a/src/HOL/Library/Float.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Library/Float.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -223,15 +223,15 @@
   done
 
 lemma transfer_numeral [transfer_rule]: 
-  "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
-  unfolding fun_rel_def cr_float_def by simp
+  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
+  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
 
 lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
   by (simp add: minus_numeral[symmetric] del: minus_numeral)
 
 lemma transfer_neg_numeral [transfer_rule]: 
-  "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
-  unfolding fun_rel_def cr_float_def by simp
+  "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
+  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
 
 lemma
   shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
isabelle