src/HOL/BNF_LFP.thy
changeset 55945 e96383acecf9
parent 55869 54ddb003e128
child 56237 69a9dfe71aed
--- a/src/HOL/BNF_LFP.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -244,14 +244,14 @@
   ultimately show P by (blast intro: assms(3))
 qed
 
-lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
-  unfolding fun_rel_def vimage2p_def by auto
+lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
+  unfolding rel_fun_def vimage2p_def by auto
 
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
-lemma id_transfer: "fun_rel A A id id"
-  unfolding fun_rel_def by simp
+lemma id_transfer: "rel_fun A A id id"
+  unfolding rel_fun_def by simp
 
 lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
   by (rule ssubst)