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 55945 e96383acecf9
parent 55565 f663fc1e653b
child 56410 a14831ac3023 
--- a/src/HOL/Library/Float.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Float.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -223,15 +223,15 @@
   done
 
 lemma transfer_numeral [transfer_rule]:
-  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
-  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
+  "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
+  unfolding rel_fun_def float.pcr_cr_eq  cr_float_def by simp
 
 lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
   by simp
 
 lemma transfer_neg_numeral [transfer_rule]:
-  "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
-  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
+  "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
+  unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp
 
 lemma
   shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
isabelle