# HG changeset patch
# User blanchet
# Date 1394116833 -3600
# Node ID e96383acecf9b28254c50fe08dcf82ba7946fd0b
# Parent  7ab8f003fe413a0f6fcfb71e356eea7e3819816f
renamed 'fun_rel' to 'rel_fun'

diff -r 7ab8f003fe41 -r e96383acecf9 NEWS
--- a/NEWS	Thu Mar 06 15:29:18 2014 +0100
+++ b/NEWS	Thu Mar 06 15:40:33 2014 +0100
@@ -195,6 +195,7 @@
     map_pair ~> map_prod
     prod_rel ~> rel_prod
     sum_rel ~> rel_sum
+    fun_rel ~> rel_fun
     set_rel ~> rel_set
     filter_rel ~> rel_filter
     fset_rel ~> rel_fset (in "Library/FSet.thy")
diff -r 7ab8f003fe41 -r e96383acecf9 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -2380,7 +2380,7 @@
     lift_definition
       rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
     is
-      "fun_rel (op =)" .
+      "rel_fun (op =)" .
 
 text {* \blankline *}
 
@@ -2423,7 +2423,7 @@
     next
       fix R S
       show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
-        by (rule, transfer) (auto simp add: fun_rel_def)
+        by (rule, transfer) (auto simp add: rel_fun_def)
     next
       fix R
       show "rel_fn R =
@@ -2431,7 +2431,7 @@
              BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
         unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
         apply transfer
-        unfolding fun_rel_def subset_iff image_iff
+        unfolding rel_fun_def subset_iff image_iff
         by auto (force, metis pair_collapse)
     qed
 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -140,8 +140,8 @@
 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
   unfolding vimage2p_def by -
 
-lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
-  unfolding fun_rel_def vimage2p_def by auto
+lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
+  unfolding rel_fun_def vimage2p_def by auto
 
 lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
   unfolding vimage2p_def convol_def by auto
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -131,9 +131,9 @@
 lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
   unfolding case_sum_o_map_sum id_comp comp_id ..
 
-lemma fun_rel_def_butlast:
-  "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
-  unfolding fun_rel_def ..
+lemma rel_fun_def_butlast:
+  "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
+  unfolding rel_fun_def ..
 
 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
   by auto
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -233,11 +233,11 @@
 lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
   unfolding image2p_def by blast
 
-lemma fun_rel_iff_geq_image2p: "fun_rel R S f g = (image2p f g R \<le> S)"
-  unfolding fun_rel_def image2p_def by auto
+lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
+  unfolding rel_fun_def image2p_def by auto
 
-lemma fun_rel_image2p: "fun_rel R (image2p f g R) f g"
-  unfolding fun_rel_def image2p_def by auto
+lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
+  unfolding rel_fun_def image2p_def by auto
 
 
 subsection {* Equivalence relations, quotients, and Hilbert's choice *}
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/BNF_LFP.thy
--- 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)
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/BNF_Util.thy
--- a/src/HOL/BNF_Util.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_Util.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -13,19 +13,19 @@
 begin
 
 definition
-  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
+  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
 where
-  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
 
-lemma fun_relI [intro]:
+lemma rel_funI [intro]:
   assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
-  shows "fun_rel A B f g"
-  using assms by (simp add: fun_rel_def)
+  shows "rel_fun A B f g"
+  using assms by (simp add: rel_fun_def)
 
-lemma fun_relD:
-  assumes "fun_rel A B f g" and "A x y"
+lemma rel_funD:
+  assumes "rel_fun A B f g" and "A x y"
   shows "B (f x) (g y)"
-  using assms by (simp add: fun_rel_def)
+  using assms by (simp add: rel_fun_def)
 
 definition collect where
 "collect F x = (\<Union>f \<in> F. f x)"
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -163,7 +163,7 @@
   map: "op \<circ>"
   sets: range
   bd: "natLeq +c |UNIV :: 'a set|"
-  rel: "fun_rel op ="
+  rel: "rel_fun op ="
 proof
   fix f show "id \<circ> f = id f" by simp
 next
@@ -193,13 +193,13 @@
   finally show "|range f| \<le>o natLeq +c ?U" .
 next
   fix R S
-  show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
+  show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
 next
   fix R
-  show "fun_rel op = R =
+  show "rel_fun op = R =
         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
-  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
+  unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
     comp_apply mem_Collect_eq split_beta bex_UNIV
   proof (safe, unfold fun_eq_iff[symmetric])
     fix x xa a b c xb y aa ba
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -76,27 +76,27 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+  "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
   by (unfold of_nat_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+  "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
 proof -
-  have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+  have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
     by (unfold of_int_of_nat [abs_def]) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
+  "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
 proof -
-  have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+  have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
     by transfer_prover
   then show ?thesis by simp
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold Num.sub_def [abs_def]) transfer_prover
 
 lemma int_of_integer_of_nat [simp]:
@@ -192,11 +192,11 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold min_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold max_def [abs_def]) transfer_prover
 
 lemma int_of_integer_min [simp]:
@@ -249,7 +249,7 @@
   [simp, code_abbrev]: "Pos = numeral"
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer numeral Pos"
+  "rel_fun HOL.eq pcr_integer numeral Pos"
   by simp transfer_prover
 
 definition Neg :: "num \<Rightarrow> integer"
@@ -257,7 +257,7 @@
   [simp, code_abbrev]: "Neg n = - Pos n"
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
+  "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
   by (simp add: Neg_def [abs_def]) transfer_prover
 
 code_datatype "0::integer" Pos Neg
@@ -680,17 +680,17 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+  "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
 proof -
-  have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+  have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
     by (unfold of_nat_def [abs_def]) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+  "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
 proof -
-  have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+  have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
     by transfer_prover
   then show ?thesis by simp
 qed
@@ -748,11 +748,11 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold min_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold max_def [abs_def]) transfer_prover
 
 lemma nat_of_natural_min [simp]:
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Int.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -78,8 +78,8 @@
     simp add: one_int.abs_eq plus_int.abs_eq)
 
 lemma int_transfer [transfer_rule]:
-  "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
-  unfolding fun_rel_def cr_int_def int_def by simp
+  "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
+  unfolding rel_fun_def cr_int_def int_def by simp
 
 lemma int_diff_cases:
   obtains (diff) m n where "z = int m - int n"
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -878,99 +878,99 @@
 
 lemma finsert_transfer [transfer_rule]:
   "(A ===> rel_fset A ===> rel_fset A) finsert finsert"
-  unfolding fun_rel_def rel_fset_alt_def by blast
+  unfolding rel_fun_def rel_fset_alt_def by blast
 
 lemma funion_transfer [transfer_rule]:
   "(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion"
-  unfolding fun_rel_def rel_fset_alt_def by blast
+  unfolding rel_fun_def rel_fset_alt_def by blast
 
 lemma ffUnion_transfer [transfer_rule]:
   "(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion"
-  unfolding fun_rel_def rel_fset_alt_def by transfer (simp, fast)
+  unfolding rel_fun_def rel_fset_alt_def by transfer (simp, fast)
 
 lemma fimage_transfer [transfer_rule]:
   "((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage"
-  unfolding fun_rel_def rel_fset_alt_def by simp blast
+  unfolding rel_fun_def rel_fset_alt_def by simp blast
 
 lemma fBall_transfer [transfer_rule]:
   "(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall"
-  unfolding rel_fset_alt_def fun_rel_def by blast
+  unfolding rel_fset_alt_def rel_fun_def by blast
 
 lemma fBex_transfer [transfer_rule]:
   "(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex"
-  unfolding rel_fset_alt_def fun_rel_def by blast
+  unfolding rel_fset_alt_def rel_fun_def by blast
 
 (* FIXME transfer doesn't work here *)
 lemma fPow_transfer [transfer_rule]:
   "(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow"
-  unfolding fun_rel_def
-  using Pow_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred]
+  unfolding rel_fun_def
+  using Pow_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred]
   by blast
 
 lemma rel_fset_transfer [transfer_rule]:
   "((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
     rel_fset rel_fset"
-  unfolding fun_rel_def
-  using rel_set_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
+  unfolding rel_fun_def
+  using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B]
   by simp
 
 lemma bind_transfer [transfer_rule]:
   "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
-  using assms unfolding fun_rel_def
-  using bind_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+  using assms unfolding rel_fun_def
+  using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 text {* Rules requiring bi-unique, bi-total or right-total relations *}
 
 lemma fmember_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(A ===> rel_fset A ===> op =) (op |\<in>|) (op |\<in>|)"
-  using assms unfolding fun_rel_def rel_fset_alt_def bi_unique_def by metis
+  using assms unfolding rel_fun_def rel_fset_alt_def bi_unique_def by metis
 
 lemma finter_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter"
-  using assms unfolding fun_rel_def
-  using inter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+  using assms unfolding rel_fun_def
+  using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 lemma fminus_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op |-|) (op |-|)"
-  using assms unfolding fun_rel_def
-  using Diff_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+  using assms unfolding rel_fun_def
+  using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 lemma fsubset_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(rel_fset A ===> rel_fset A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
-  using assms unfolding fun_rel_def
-  using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+  using assms unfolding rel_fun_def
+  using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 lemma fSup_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
-  using assms unfolding fun_rel_def
+  using assms unfolding rel_fun_def
   apply clarify
   apply transfer'
-  using Sup_fset_transfer[unfolded fun_rel_def] by blast
+  using Sup_fset_transfer[unfolded rel_fun_def] by blast
 
 (* FIXME: add right_total_fInf_transfer *)
 
 lemma fInf_transfer [transfer_rule]:
   assumes "bi_unique A" and "bi_total A"
   shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf"
-  using assms unfolding fun_rel_def
+  using assms unfolding rel_fun_def
   apply clarify
   apply transfer'
-  using Inf_fset_transfer[unfolded fun_rel_def] by blast
+  using Inf_fset_transfer[unfolded rel_fun_def] by blast
 
 lemma ffilter_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
-  using assms unfolding fun_rel_def
-  using Lifting_Set.filter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+  using assms unfolding rel_fun_def
+  using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 lemma card_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
-  using assms unfolding fun_rel_def
-  using card_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+  using assms unfolding rel_fun_def
+  using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 end
 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Library/Float.thy
--- 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)"
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -33,7 +33,7 @@
 definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
 
 lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" 
-unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split)
+unfolding rel_fun_def rel_option_iff equal_None_def by (auto split: option.split)
 
 lemma dom_transfer:
   assumes [transfer_rule]: "bi_total A"
@@ -55,7 +55,7 @@
 lemma bulkload_transfer: 
   "(list_all2 A ===> op= ===> rel_option A) 
     (\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
-unfolding fun_rel_def 
+unfolding rel_fun_def 
 apply clarsimp 
 apply (erule list_all2_induct) 
   apply simp 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -2289,7 +2289,7 @@
 interpretation lifting_syntax .
 
 lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
-  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
+  unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto
 
 end
 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Quotient_Set.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -50,7 +50,7 @@
 lemma collect_rsp[quot_respect]:
   assumes "Quotient3 R Abs Rep"
   shows "((R ===> op =) ===> rel_vset R) Collect Collect"
-  by (intro fun_relI) (simp add: fun_rel_def rel_vset_def)
+  by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
 
 lemma collect_prs[quot_preserve]:
   assumes "Quotient3 R Abs Rep"
@@ -61,7 +61,7 @@
 lemma union_rsp[quot_respect]:
   assumes "Quotient3 R Abs Rep"
   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
-  by (intro fun_relI) (simp add: rel_vset_def)
+  by (intro rel_funI) (simp add: rel_vset_def)
 
 lemma union_prs[quot_preserve]:
   assumes "Quotient3 R Abs Rep"
@@ -72,7 +72,7 @@
 lemma diff_rsp[quot_respect]:
   assumes "Quotient3 R Abs Rep"
   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
-  by (intro fun_relI) (simp add: rel_vset_def)
+  by (intro rel_funI) (simp add: rel_vset_def)
 
 lemma diff_prs[quot_preserve]:
   assumes "Quotient3 R Abs Rep"
@@ -83,7 +83,7 @@
 lemma inter_rsp[quot_respect]:
   assumes "Quotient3 R Abs Rep"
   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
-  by (intro fun_relI) (auto simp add: rel_vset_def)
+  by (intro rel_funI) (auto simp add: rel_vset_def)
 
 lemma inter_prs[quot_preserve]:
   assumes "Quotient3 R Abs Rep"
@@ -98,6 +98,6 @@
 
 lemma mem_rsp[quot_respect]:
   shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
-  by (intro fun_relI) (simp add: rel_vset_def)
+  by (intro rel_funI) (simp add: rel_vset_def)
 
 end
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Library/Quotient_Syntax.thy
--- a/src/HOL/Library/Quotient_Syntax.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -11,6 +11,6 @@
 notation
   rel_conj (infixr "OOO" 75) and
   map_fun (infixr "--->" 55) and
-  fun_rel (infixr "===>" 55)
+  rel_fun (infixr "===>" 55)
 
 end
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -52,7 +52,7 @@
   assumes [transfer_rule]: "right_total B"
   assumes [transfer_rule]: "bi_unique A"
   shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
-using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
+using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
 by metis
 
 lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
@@ -69,7 +69,7 @@
 
 lemma left_total_fun:
   "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
-  unfolding left_total_def fun_rel_def
+  unfolding left_total_def rel_fun_def
   apply (rule allI, rename_tac f)
   apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
   apply clarify
@@ -83,7 +83,7 @@
 
 lemma left_unique_fun:
   "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
-  unfolding left_total_def left_unique_def fun_rel_def
+  unfolding left_total_def left_unique_def rel_fun_def
   by (clarify, rule ext, fast)
 
 lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
@@ -242,7 +242,7 @@
   assumes 2: "Quotient R2 abs2 rep2 T2"
   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
   using assms unfolding Quotient_alt_def2
-  unfolding fun_rel_def fun_eq_iff map_fun_apply
+  unfolding rel_fun_def fun_eq_iff map_fun_apply
   by (safe, metis+)
 
 lemma apply_rsp:
@@ -250,12 +250,12 @@
   assumes q: "Quotient R1 Abs1 Rep1 T1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by (auto elim: fun_relE)
+  using a by (auto elim: rel_funE)
 
 lemma apply_rsp':
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by (auto elim: fun_relE)
+  using a by (auto elim: rel_funE)
 
 lemma apply_rsp'':
   assumes "Quotient R Abs Rep T"
@@ -296,12 +296,12 @@
   shows "x = y"
 using assms by (simp add: invariant_def)
 
-lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
-unfolding invariant_def fun_rel_def by auto
+lemma rel_fun_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
+unfolding invariant_def rel_fun_def by auto
 
-lemma fun_rel_invariant_rel:
+lemma rel_fun_invariant_rel:
   shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
-by (auto simp add: invariant_def fun_rel_def)
+by (auto simp add: invariant_def rel_fun_def)
 
 lemma invariant_same_args:
   shows "invariant P x x \<equiv> P x"
@@ -376,7 +376,7 @@
   using 1 unfolding Quotient_alt_def right_total_def by metis
 
 lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
-  using 1 unfolding Quotient_alt_def fun_rel_def by simp
+  using 1 unfolding Quotient_alt_def rel_fun_def by simp
 
 lemma Quotient_abs_induct:
   assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
@@ -395,7 +395,7 @@
   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
 
 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
-  using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
+  using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
 
 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
   using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
@@ -432,7 +432,7 @@
   by blast
 
 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
-  unfolding fun_rel_def T_def by simp
+  unfolding rel_fun_def T_def by simp
 
 end
 
@@ -557,10 +557,10 @@
   assumes "A \<ge> C"
   assumes "B \<le> D"
   shows   "(A ===> B) \<le> (C ===> D)"
-using assms unfolding fun_rel_def by blast
+using assms unfolding rel_fun_def by blast
 
 lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
-unfolding OO_def fun_rel_def by blast
+unfolding OO_def rel_fun_def by blast
 
 lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
 unfolding right_unique_def left_total_def by blast
@@ -573,7 +573,7 @@
 assumes 2: "right_unique R'" "left_total R'"
 shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
   using functional_relation[OF 2] functional_converse_relation[OF 1]
-  unfolding fun_rel_def OO_def
+  unfolding rel_fun_def OO_def
   apply clarify
   apply (subst all_comm)
   apply (subst all_conj_distrib[symmetric])
@@ -585,7 +585,7 @@
 assumes 2: "left_unique S'" "right_total S'"
 shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
   using functional_converse_relation[OF 2] functional_relation[OF 1]
-  unfolding fun_rel_def OO_def
+  unfolding rel_fun_def OO_def
   apply clarify
   apply (subst all_comm)
   apply (subst all_conj_distrib[symmetric])
@@ -599,7 +599,7 @@
   assumes "(R ===> op=) P P'"
   assumes "Domainp R = P''"
   shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
-using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def invariant_def
 fun_eq_iff by blast
 
 lemma composed_equiv_rel_eq_invariant:
@@ -615,7 +615,7 @@
   assumes "(A ===> op=) P' P"
   shows "Domainp (A OO B) = P'"
 using assms
-unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def 
+unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def 
 by (fast intro: fun_eq_iff)
 
 lemma pcr_Domainp_par:
@@ -623,7 +623,7 @@
 assumes "Domainp A = P1"
 assumes "(A ===> op=) P2' P2"
 shows "Domainp (A OO B) = (inf P1 P2')"
-using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
+using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def
 by (fast intro: fun_eq_iff)
 
 definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Lifting_Option.thy
--- a/src/HOL/Lifting_Option.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -86,11 +86,11 @@
   by (rule option.rel_inject)
 
 lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma case_option_transfer [transfer_rule]:
   "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
-  unfolding fun_rel_def split_option_all by simp
+  unfolding rel_fun_def split_option_all by simp
 
 lemma map_option_transfer [transfer_rule]:
   "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
@@ -99,7 +99,7 @@
 lemma option_bind_transfer [transfer_rule]:
   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
     Option.bind Option.bind"
-  unfolding fun_rel_def split_option_all by simp
+  unfolding rel_fun_def split_option_all by simp
 
 end
 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Product.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -80,17 +80,17 @@
 interpretation lifting_syntax .
 
 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma case_prod_transfer [transfer_rule]:
   "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma curry_transfer [transfer_rule]:
   "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
@@ -104,7 +104,7 @@
 lemma rel_prod_transfer [transfer_rule]:
   "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
     rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
-  unfolding fun_rel_def by auto
+  unfolding rel_fun_def by auto
 
 end
 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Set.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -109,19 +109,19 @@
 
 lemma insert_transfer [transfer_rule]:
   "(A ===> rel_set A ===> rel_set A) insert insert"
-  unfolding fun_rel_def rel_set_def by auto
+  unfolding rel_fun_def rel_set_def by auto
 
 lemma union_transfer [transfer_rule]:
   "(rel_set A ===> rel_set A ===> rel_set A) union union"
-  unfolding fun_rel_def rel_set_def by auto
+  unfolding rel_fun_def rel_set_def by auto
 
 lemma Union_transfer [transfer_rule]:
   "(rel_set (rel_set A) ===> rel_set A) Union Union"
-  unfolding fun_rel_def rel_set_def by simp fast
+  unfolding rel_fun_def rel_set_def by simp fast
 
 lemma image_transfer [transfer_rule]:
   "((A ===> B) ===> rel_set A ===> rel_set B) image image"
-  unfolding fun_rel_def rel_set_def by simp fast
+  unfolding rel_fun_def rel_set_def by simp fast
 
 lemma UNION_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
@@ -129,15 +129,15 @@
 
 lemma Ball_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
-  unfolding rel_set_def fun_rel_def by fast
+  unfolding rel_set_def rel_fun_def by fast
 
 lemma Bex_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> op =) ===> op =) Bex Bex"
-  unfolding rel_set_def fun_rel_def by fast
+  unfolding rel_set_def rel_fun_def by fast
 
 lemma Pow_transfer [transfer_rule]:
   "(rel_set A ===> rel_set (rel_set A)) Pow Pow"
-  apply (rule fun_relI, rename_tac X Y, rule rel_setI)
+  apply (rule rel_funI, rename_tac X Y, rule rel_setI)
   apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
   apply (simp add: rel_set_def, fast)
   apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
@@ -147,16 +147,16 @@
 lemma rel_set_transfer [transfer_rule]:
   "((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =)
     rel_set rel_set"
-  unfolding fun_rel_def rel_set_def by fast
+  unfolding rel_fun_def rel_set_def by fast
 
 lemma SUPR_parametric [transfer_rule]:
   "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
-proof(rule fun_relI)+
+proof(rule rel_funI)+
   fix A B f and g :: "'b \<Rightarrow> 'c"
   assume AB: "rel_set R A B"
     and fg: "(R ===> op =) f g"
   show "SUPR A f = SUPR B g"
-    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
+    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] rel_funD[OF fg] intro: rev_bexI)
 qed
 
 lemma bind_transfer [transfer_rule]:
@@ -168,27 +168,27 @@
 lemma member_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(A ===> rel_set A ===> op =) (op \<in>) (op \<in>)"
-  using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
+  using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
 
 lemma right_total_Collect_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> op =) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
-  using assms unfolding right_total_def rel_set_def fun_rel_def Domainp_iff by fast
+  using assms unfolding right_total_def rel_set_def rel_fun_def Domainp_iff by fast
 
 lemma Collect_transfer [transfer_rule]:
   assumes "bi_total A"
   shows "((A ===> op =) ===> rel_set A) Collect Collect"
-  using assms unfolding fun_rel_def rel_set_def bi_total_def by fast
+  using assms unfolding rel_fun_def rel_set_def bi_total_def by fast
 
 lemma inter_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter"
-  using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
+  using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
 
 lemma Diff_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(rel_set A ===> rel_set A ===> rel_set A) (op -) (op -)"
-  using assms unfolding fun_rel_def rel_set_def bi_unique_def
+  using assms unfolding rel_fun_def rel_set_def bi_unique_def
   unfolding Ball_def Bex_def Diff_eq
   by (safe, simp, metis, simp, metis)
 
@@ -232,7 +232,7 @@
 lemma filter_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
-  unfolding Set.filter_def[abs_def] fun_rel_def rel_set_def by blast
+  unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast
 
 lemma bi_unique_rel_set_lemma:
   assumes "bi_unique R" and "rel_set R X Y"
@@ -270,12 +270,12 @@
 
 lemma finite_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
-  by (rule fun_relI, erule (1) bi_unique_rel_set_lemma,
+  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma,
     auto dest: finite_imageD)
 
 lemma card_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
-  by (rule fun_relI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
+  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
 
 lemma vimage_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_unique B"
@@ -285,7 +285,7 @@
 lemma setsum_parametric [transfer_rule]:
   assumes "bi_unique A"
   shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
-proof(rule fun_relI)+
+proof(rule rel_funI)+
   fix f :: "'a \<Rightarrow> 'c" and g S T
   assume fg: "(A ===> op =) f g"
     and ST: "rel_set A S T"
@@ -313,7 +313,7 @@
     assume "t \<in> T"
     with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
     hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
-    moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
+    moreover from fg `A s t` have "f s = g t" by(rule rel_funD)
     ultimately show "g t = f (?f t)" by simp
   qed
 qed
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Lifting_Sum.thy
--- a/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -70,14 +70,14 @@
 interpretation lifting_syntax .
 
 lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma case_sum_transfer [transfer_rule]:
   "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
-  unfolding fun_rel_def rel_sum_def by (simp split: sum.split)
+  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
 
 end
 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/List.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -6713,17 +6713,17 @@
 
 lemma Cons_transfer [transfer_rule]:
   "(A ===> list_all2 A ===> list_all2 A) Cons Cons"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma case_list_transfer [transfer_rule]:
   "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
     case_list case_list"
-  unfolding fun_rel_def by (simp split: list.split)
+  unfolding rel_fun_def by (simp split: list.split)
 
 lemma rec_list_transfer [transfer_rule]:
   "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
     rec_list rec_list"
-  unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
+  unfolding rel_fun_def by (clarify, erule list_all2_induct, simp_all)
 
 lemma tl_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A) tl tl"
@@ -6731,7 +6731,7 @@
 
 lemma butlast_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A) butlast butlast"
-  by (rule fun_relI, erule list_all2_induct, auto)
+  by (rule rel_funI, erule list_all2_induct, auto)
 
 lemma set_transfer [transfer_rule]:
   "(list_all2 A ===> rel_set A) set set"
@@ -6836,7 +6836,7 @@
 lemma remdups_adj_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "(list_all2 A ===> list_all2 A) remdups_adj remdups_adj"
-  proof (rule fun_relI, erule list_all2_induct)
+  proof (rule rel_funI, erule list_all2_induct)
   qed (auto simp: remdups_adj_Cons assms[unfolded bi_unique_def] split: list.splits)
 
 lemma replicate_transfer [transfer_rule]:
@@ -6874,7 +6874,7 @@
 
 lemma lists_transfer [transfer_rule]:
   "(rel_set A ===> rel_set (list_all2 A)) lists lists"
-  apply (rule fun_relI, rule rel_setI)
+  apply (rule rel_funI, rule rel_setI)
   apply (erule lists.induct, simp)
   apply (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
   apply (erule lists.induct, simp)
@@ -6884,7 +6884,7 @@
 lemma set_Cons_transfer [transfer_rule]:
   "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
     set_Cons set_Cons"
-  unfolding fun_rel_def rel_set_def set_Cons_def
+  unfolding rel_fun_def rel_set_def set_Cons_def
   apply safe
   apply (simp add: list_all2_Cons1, fast)
   apply (simp add: list_all2_Cons2, fast)
@@ -6896,7 +6896,7 @@
 
 lemma null_transfer [transfer_rule]:
   "(list_all2 A ===> op =) List.null List.null"
-  unfolding fun_rel_def List.null_def by auto
+  unfolding rel_fun_def List.null_def by auto
 
 lemma list_all_transfer [transfer_rule]:
   "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
@@ -6908,9 +6908,9 @@
 
 lemma splice_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
-  apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
-  apply (rule fun_relI)
-  apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
+  apply (rule rel_funI, erule list_all2_induct, simp add: rel_fun_def, simp)
+  apply (rule rel_funI)
+  apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def)
   done
 
 lemma listsum_transfer[transfer_rule]:
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Quotient.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -146,7 +146,7 @@
     using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
   moreover
   have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
-    by (rule fun_relI)
+    by (rule rel_funI)
       (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
         simp (no_asm) add: Quotient3_def, simp)
   
@@ -157,17 +157,17 @@
         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   proof -
     
-    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
+    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding rel_fun_def
       using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
       by (metis (full_types) part_equivp_def)
-    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
+    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding rel_fun_def
       using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
       by (metis (full_types) part_equivp_def)
     moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
-      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
+      apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
     moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
         (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
-      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
+      apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
     by (metis map_fun_apply)
   
     ultimately show ?thesis by blast
@@ -204,7 +204,7 @@
   assumes q: "Quotient3 R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by (auto elim: fun_relE)
+  using a by (auto elim: rel_funE)
 
 lemma apply_rspQ3'':
   assumes "Quotient3 R Abs Rep"
@@ -261,7 +261,7 @@
   apply(rule iffI)
   apply(rule allI)
   apply(drule_tac x="\<lambda>y. f x" in bspec)
-  apply(simp add: in_respects fun_rel_def)
+  apply(simp add: in_respects rel_fun_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply (auto elim: equivpE reflpE)
@@ -273,7 +273,7 @@
   apply(auto)
   apply(rule_tac x="\<lambda>y. f x" in bexI)
   apply(simp)
-  apply(simp add: Respects_def in_respects fun_rel_def)
+  apply(simp add: Respects_def in_respects rel_fun_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply (auto elim: equivpE reflpE)
@@ -326,10 +326,10 @@
   assumes q: "Quotient3 R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
-  apply (auto simp add: Babs_def in_respects fun_rel_def)
+  apply (auto simp add: Babs_def in_respects rel_fun_def)
   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
-  using a apply (simp add: Babs_def fun_rel_def)
-  apply (simp add: in_respects fun_rel_def)
+  using a apply (simp add: Babs_def rel_fun_def)
+  apply (simp add: in_respects rel_fun_def)
   using Quotient3_rel[OF q]
   by metis
 
@@ -349,7 +349,7 @@
   shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   apply(rule iffI)
   apply(simp_all only: babs_rsp[OF q])
-  apply(auto simp add: Babs_def fun_rel_def)
+  apply(auto simp add: Babs_def rel_fun_def)
   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   apply(metis Babs_def)
   apply (simp add: in_respects)
@@ -367,17 +367,17 @@
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ball (Respects R) f = Ball (Respects R) g"
-  using a by (auto simp add: Ball_def in_respects elim: fun_relE)
+  using a by (auto simp add: Ball_def in_respects elim: rel_funE)
 
 lemma bex_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
-  using a by (auto simp add: Bex_def in_respects elim: fun_relE)
+  using a by (auto simp add: Bex_def in_respects elim: rel_funE)
 
 lemma bex1_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
-  using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
+  using a by (auto elim: rel_funE simp add: Ex1_def in_respects) 
 
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
@@ -440,7 +440,7 @@
 lemma bex1_rel_rsp:
   assumes a: "Quotient3 R absf repf"
   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
-  apply (simp add: fun_rel_def)
+  apply (simp add: rel_fun_def)
   apply clarify
   apply rule
   apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
@@ -519,7 +519,7 @@
 lemma quot_rel_rsp:
   assumes a: "Quotient3 R Abs Rep"
   shows "(R ===> R ===> op =) R R"
-  apply(rule fun_relI)+
+  apply(rule rel_funI)+
   apply(rule equals_rsp[OF a])
   apply(assumption)+
   done
@@ -536,7 +536,7 @@
 lemma o_rsp:
   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
-  by (force elim: fun_relE)+
+  by (force elim: rel_funE)+
 
 lemma cond_prs:
   assumes a: "Quotient3 R absf repf"
@@ -563,7 +563,7 @@
 
 lemma let_rsp:
   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
-  by (force elim: fun_relE)
+  by (force elim: rel_funE)
 
 lemma id_rsp:
   shows "(R ===> R) id id"
@@ -759,7 +759,7 @@
 ML_file "Tools/Quotient/quotient_info.ML"
 setup Quotient_Info.setup
 
-declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
+declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
 
 lemmas [quot_thm] = fun_quotient3
 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -403,7 +403,7 @@
 
 lemma Cons_rsp2 [quot_respect]:
   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
-  apply (auto intro!: fun_relI)
+  apply (auto intro!: rel_funI)
   apply (rule_tac b="x # b" in relcomppI)
   apply auto
   apply (rule_tac b="x # ba" in relcomppI)
@@ -459,24 +459,24 @@
 lemma compositional_rsp3:
   assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
   shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
-  by (auto intro!: fun_relI)
-     (metis (full_types) assms fun_relE relcomppI)
+  by (auto intro!: rel_funI)
+     (metis (full_types) assms rel_funE relcomppI)
 
 lemma append_rsp2 [quot_respect]:
   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
   by (intro compositional_rsp3)
-     (auto intro!: fun_relI simp add: append_rsp2_pre)
+     (auto intro!: rel_funI simp add: append_rsp2_pre)
 
 lemma map_rsp2 [quot_respect]:
   "((op \<approx> ===> op \<approx>) ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) map map"
-proof (auto intro!: fun_relI)
+proof (auto intro!: rel_funI)
   fix f f' :: "'a list \<Rightarrow> 'b list"
   fix xa ya x y :: "'a list list"
   assume fs: "(op \<approx> ===> op \<approx>) f f'" and x: "list_all2 op \<approx> xa x" and xy: "set x = set y" and y: "list_all2 op \<approx> y ya"
   have a: "(list_all2 op \<approx>) (map f xa) (map f x)"
     using x
     by (induct xa x rule: list_induct2')
-       (simp_all, metis fs fun_relE list_eq_def)
+       (simp_all, metis fs rel_funE list_eq_def)
   have b: "set (map f x) = set (map f y)"
     using xy fs
     by (induct x y rule: list_induct2')
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Real.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -389,7 +389,7 @@
 lemma eq_Real:
   "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
   using real.rel_eq_transfer
-  unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
+  unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp
 
 lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
 by (simp add: real.domain_eq realrel_def)
@@ -445,13 +445,13 @@
   assumes X: "cauchy X" and Y: "cauchy Y"
   shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
   using assms plus_real.transfer
-  unfolding cr_real_eq fun_rel_def by simp
+  unfolding cr_real_eq rel_fun_def by simp
 
 lemma minus_Real:
   assumes X: "cauchy X"
   shows "- Real X = Real (\<lambda>n. - X n)"
   using assms uminus_real.transfer
-  unfolding cr_real_eq fun_rel_def by simp
+  unfolding cr_real_eq rel_fun_def by simp
 
 lemma diff_Real:
   assumes X: "cauchy X" and Y: "cauchy Y"
@@ -463,14 +463,14 @@
   assumes X: "cauchy X" and Y: "cauchy Y"
   shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
   using assms times_real.transfer
-  unfolding cr_real_eq fun_rel_def by simp
+  unfolding cr_real_eq rel_fun_def by simp
 
 lemma inverse_Real:
   assumes X: "cauchy X"
   shows "inverse (Real X) =
     (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
   using assms inverse_real.transfer zero_real.transfer
-  unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)
+  unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis)
 
 instance proof
   fix a b c :: real
@@ -546,7 +546,7 @@
   assumes X: "cauchy X"
   shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
   using assms positive.transfer
-  unfolding cr_real_eq fun_rel_def by simp
+  unfolding cr_real_eq rel_fun_def by simp
 
 lemma positive_zero: "\<not> positive 0"
   by transfer auto
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -1260,12 +1260,12 @@
 
         fun mk_map_transfer () =
           let
-            val rels = map2 mk_fun_rel transfer_domRs transfer_ranRs;
-            val rel = mk_fun_rel
+            val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
+            val rel = mk_rel_fun
               (Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs))
               (Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs));
             val concl = HOLogic.mk_Trueprop
-              (fold_rev mk_fun_rel rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
+              (fold_rev mk_rel_fun rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -195,8 +195,8 @@
           @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
       set_maps;
   in
-    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
-    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
+    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
+    unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
       rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
       REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -502,9 +502,9 @@
     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
     fun flip f x y = if fp = Greatest_FP then f y x else f x y;
 
-    val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis;
+    val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis;
     fun mk_transfer relphi pre_phi un_fold un_fold' =
-      fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold';
+      fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
     val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
 
     val goal = fold_rev Logic.all (phis @ pre_phis)
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -1088,16 +1088,16 @@
     val n = length map_transfers;
   in
     unfold_thms_tac ctxt
-      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
-    unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
+      @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+    unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN
     HEADGOAL (EVERY'
       [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct,
       EVERY' (map (fn map_transfer => EVERY'
         [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt unfolds),
-        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
+        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
         REPEAT_DETERM_N m o rtac @{thm id_transfer},
-        REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
+        REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
         etac @{thm predicate2D}, etac @{thm image2pI}])
       map_transfers)])
   end;
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -788,17 +788,17 @@
     val n = length map_transfers;
   in
     unfold_thms_tac ctxt
-      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
-    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
+      @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+    unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY'
       [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_induct,
       EVERY' (map (fn map_transfer => EVERY'
         [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
         SELECT_GOAL (unfold_thms_tac ctxt folds),
         etac @{thm predicate2D_vimage2p},
-        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
+        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
         REPEAT_DETERM_N m o rtac @{thm id_transfer},
-        REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel},
+        REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
         atac])
       map_transfers)])
   end;
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -94,7 +94,7 @@
   val mk_cprod: term -> term -> term
   val mk_csum: term -> term -> term
   val mk_dir_image: term -> term -> term
-  val mk_fun_rel: term -> term -> term
+  val mk_rel_fun: term -> term -> term
   val mk_image: term -> term
   val mk_in: term list -> term list -> typ -> term
   val mk_leq: term -> term -> term
@@ -438,11 +438,11 @@
   let val (T, U) = dest_funT (fastype_of f);
   in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
 
-fun mk_fun_rel R S =
+fun mk_rel_fun R S =
   let
     val ((RA, RB), RT) = `dest_pred2T (fastype_of R);
     val ((SA, SB), ST) = `dest_pred2T (fastype_of S);
-  in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
+  in Const (@{const_name rel_fun}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
 
 (*FIXME: "x"?*)
 (*(nth sets i) must be of type "T --> 'ai set"*)
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -166,11 +166,11 @@
 fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
   | get_binder_types _ = []
 
-fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
+fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
     (T, V) :: get_binder_types_by_rel S (U, W)
   | get_binder_types_by_rel _ _ = []
 
-fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
+fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
     get_body_type_by_rel S (U, V)
   | get_body_type_by_rel _ (U, V)  = (U, V)
 
@@ -270,8 +270,8 @@
       let
         val thy = Proof_Context.theory_of ctxt
         val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
-        val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
-        val rep_abs_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs_eq}
+        val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
+        val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
       in
         case mono_eq_prover ctxt (hd(prems_of rep_abs_thm)) of
           SOME mono_eq_thm =>
@@ -311,7 +311,7 @@
           end
       in
         rep_abs_folded_unmapped_thm
-        |> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args
+        |> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args
         |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
       end
     
@@ -505,11 +505,11 @@
     fun simp_arrows_conv ctm =
       let
         val unfold_conv = Conv.rewrs_conv 
-          [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, 
-            @{thm fun_rel_invariant_rel[THEN eq_reflection]},
-            @{thm fun_rel_eq[THEN eq_reflection]},
-            @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
-            @{thm fun_rel_def[THEN eq_reflection]}]
+          [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, 
+            @{thm rel_fun_invariant_rel[THEN eq_reflection]},
+            @{thm rel_fun_eq[THEN eq_reflection]},
+            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
+            @{thm rel_fun_def[THEN eq_reflection]}]
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
         val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
             invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
@@ -522,7 +522,7 @@
           (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
       in
         case (Thm.term_of ctm) of
-          Const (@{const_name "fun_rel"}, _) $ _ $ _ => 
+          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
             (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
           | _ => (invariant_commute_conv then_conv relator_eq_conv) ctm
       end
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -27,7 +27,7 @@
   val same_type_constrs: typ * typ -> bool
   val Targs: typ -> typ list
   val Tname: typ -> string
-  val is_fun_rel: term -> bool
+  val is_rel_fun: term -> bool
   val relation_types: typ -> typ * typ
   val mk_HOL_eq: thm -> thm
   val safe_HOL_meta_eq: thm -> thm
@@ -110,8 +110,8 @@
 fun Tname (Type (name, _)) = name
   | Tname _ = ""
 
-fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
-  | is_fun_rel _ = false
+fun is_rel_fun (Const (@{const_name "rel_fun"}, _) $ _ $ _) = true
+  | is_rel_fun _ = false
 
 fun relation_types typ = 
   case strip_type typ of
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -109,13 +109,13 @@
     fun simp_arrows_conv ctm =
       let
         val unfold_conv = Conv.rewrs_conv 
-          [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
-            @{thm fun_rel_def[THEN eq_reflection]}]
+          [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
+            @{thm rel_fun_def[THEN eq_reflection]}]
         val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
       in
         case (Thm.term_of ctm) of
-          Const (@{const_name fun_rel}, _) $ _ $ _ => 
+          Const (@{const_name rel_fun}, _) $ _ $ _ => 
             (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
           | _ => Conv.all_conv ctm
       end
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -114,11 +114,11 @@
 fun ball_bex_range_simproc ctxt redex =
   case redex of
     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
-      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+      (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
         calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 
   | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
-      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+      (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
         calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 
   | _ => NONE
@@ -306,7 +306,7 @@
    The deterministic part:
     - remove lambdas from both sides
     - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
-    - prove Ball/Bex relations using fun_relI
+    - prove Ball/Bex relations using rel_funI
     - reflexivity of equality
     - prove equality of relations using equals_rsp
     - use user-supplied RSP theorems
@@ -324,8 +324,8 @@
 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
   (case bare_concl goal of
       (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
-    (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
-        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+    (Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
 
       (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   | (Const (@{const_name HOL.eq},_) $
@@ -334,10 +334,10 @@
         => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
 
       (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
-  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
       (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
       (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
 
       (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   | Const (@{const_name HOL.eq},_) $
@@ -346,12 +346,12 @@
         => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
 
       (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
-  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
       (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
       (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
 
-  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
       (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
         => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
 
@@ -369,7 +369,7 @@
   | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
 
      (* respectfulness of constants; in particular of a simple relation *)
-  | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
+  | _ $ (Const _) $ (Const _)  (* rel_fun, list_rel, etc but not equality *)
       => resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
 
       (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/transfer.ML	Thu Mar 06 15:40:33 2014 +0100
@@ -389,7 +389,7 @@
           val r2 = rel T2 U2
           val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
         in
-          Const (@{const_name fun_rel}, rT) $ r1 $ r2
+          Const (@{const_name rel_fun}, rT) $ r1 $ r2
         end
       | rel T U =
         let
@@ -617,7 +617,7 @@
     val rule1 = transfer_rule_of_term ctxt false rhs
     val rules = get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
-    val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm fun_rel_eq[symmetric,THEN eq_reflection]}])
+    val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
   in
     EVERY
       [CONVERSION prep_conv i,
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -2363,23 +2363,23 @@
   fix F G
   assume "rel_filter T F G"
   thus "filtermap Abs F = G" unfolding filter_eq_iff
-    by(auto simp add: eventually_filtermap rel_filter_eventually * fun_relI del: iffI elim!: fun_relD)
+    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
 next
   from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
 
   fix F
   show "rel_filter T (filtermap Rep F) F" 
-    by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI
+    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
             del: iffI simp add: eventually_filtermap rel_filter_eventually)
 qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
          fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
 
 lemma eventually_parametric [transfer_rule]:
   "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
-by(simp add: fun_rel_def rel_filter_eventually)
+by(simp add: rel_fun_def rel_filter_eventually)
 
 lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
-by(auto simp add: rel_filter_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
+by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
 
 lemma rel_filter_mono [relator_mono]:
   "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
@@ -2387,7 +2387,7 @@
 by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
 
 lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff fun_rel_def)
+by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
 
 lemma is_filter_parametric_aux:
   assumes "is_filter F"
@@ -2427,11 +2427,11 @@
 lemma is_filter_parametric [transfer_rule]:
   "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
   \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
-apply(rule fun_relI)
+apply(rule rel_funI)
 apply(rule iffI)
  apply(erule (3) is_filter_parametric_aux)
 apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: fun_rel_def)
+apply(auto simp add: rel_fun_def)
 done
 
 lemma left_total_rel_filter [reflexivity_rule]:
@@ -2490,15 +2490,15 @@
 by(simp add: rel_filter_eventually All_transfer)
 
 lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
-by(simp add: rel_filter_eventually fun_rel_def)
+by(simp add: rel_filter_eventually rel_fun_def)
 
 lemma sup_filter_parametric [transfer_rule]:
   "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
-by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: fun_relD)
+by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
 
 lemma Sup_filter_parametric [transfer_rule]:
   "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
-proof(rule fun_relI)
+proof(rule rel_funI)
   fix S T
   assume [transfer_rule]: "rel_set (rel_filter A) S T"
   show "rel_filter A (Sup S) (Sup T)"
@@ -2507,7 +2507,7 @@
 
 lemma principal_parametric [transfer_rule]:
   "(rel_set A ===> rel_filter A) principal principal"
-proof(rule fun_relI)
+proof(rule rel_funI)
   fix S S'
   assume [transfer_rule]: "rel_set A S S'"
   show "rel_filter A (principal S) (principal S')"
@@ -2537,7 +2537,7 @@
 
 lemma inf_filter_parametric [transfer_rule]:
   "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
-proof(intro fun_relI)+
+proof(intro rel_funI)+
   fix F F' G G'
   assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
   have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Transfer.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -13,7 +13,7 @@
 
 locale lifting_syntax
 begin
-  notation fun_rel (infixr "===>" 55)
+  notation rel_fun (infixr "===>" 55)
   notation map_fun (infixr "--->" 55)
 end
 
@@ -21,21 +21,21 @@
 begin
 interpretation lifting_syntax .
 
-lemma fun_relD2:
-  assumes "fun_rel A B f g" and "A x x"
+lemma rel_funD2:
+  assumes "rel_fun A B f g" and "A x x"
   shows "B (f x) (g x)"
-  using assms by (rule fun_relD)
+  using assms by (rule rel_funD)
 
-lemma fun_relE:
-  assumes "fun_rel A B f g" and "A x y"
+lemma rel_funE:
+  assumes "rel_fun A B f g" and "A x y"
   obtains "B (f x) (g y)"
-  using assms by (simp add: fun_rel_def)
+  using assms by (simp add: rel_fun_def)
 
-lemmas fun_rel_eq = fun.rel_eq
+lemmas rel_fun_eq = fun.rel_eq
 
-lemma fun_rel_eq_rel:
-shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
-  by (simp add: fun_rel_def)
+lemma rel_fun_eq_rel:
+shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+  by (simp add: rel_fun_def)
 
 
 subsection {* Transfer method *}
@@ -98,12 +98,12 @@
 lemma Rel_app:
   assumes "Rel (A ===> B) f g" and "Rel A x y"
   shows "Rel B (f x) (g y)"
-  using assms unfolding Rel_def fun_rel_def by fast
+  using assms unfolding Rel_def rel_fun_def by fast
 
 lemma Rel_abs:
   assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
-  using assms unfolding Rel_def fun_rel_def by fast
+  using assms unfolding Rel_def rel_fun_def by fast
 
 end
 
@@ -112,7 +112,7 @@
 
 declare refl [transfer_rule]
 
-declare fun_rel_eq [relator_eq]
+declare rel_fun_eq [relator_eq]
 
 hide_const (open) Rel
 
@@ -131,7 +131,7 @@
 lemma Domainp_prod_fun_eq[transfer_domain_rule]:
   assumes "Domainp T = P"
   shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))"
-by (auto intro: choice simp: assms[symmetric] Domainp_iff fun_rel_def fun_eq_iff)
+by (auto intro: choice simp: assms[symmetric] Domainp_iff rel_fun_def fun_eq_iff)
 
 subsection {* Predicates on relations, i.e. ``class constraints'' *}
 
@@ -163,7 +163,7 @@
 
 lemma right_total_alt_def:
   "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
-  unfolding right_total_def fun_rel_def
+  unfolding right_total_def rel_fun_def
   apply (rule iffI, fast)
   apply (rule allI)
   apply (drule_tac x="\<lambda>x. True" in spec)
@@ -173,11 +173,11 @@
 
 lemma right_unique_alt_def:
   "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
-  unfolding right_unique_def fun_rel_def by auto
+  unfolding right_unique_def rel_fun_def by auto
 
 lemma bi_total_alt_def:
   "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
-  unfolding bi_total_def fun_rel_def
+  unfolding bi_total_def rel_fun_def
   apply (rule iffI, fast)
   apply safe
   apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
@@ -190,7 +190,7 @@
 
 lemma bi_unique_alt_def:
   "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
-  unfolding bi_unique_def fun_rel_def by auto
+  unfolding bi_unique_def rel_fun_def by auto
 
 lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
 by(auto simp add: bi_unique_def)
@@ -234,7 +234,7 @@
 
 lemma right_total_fun [transfer_rule]:
   "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
-  unfolding right_total_def fun_rel_def
+  unfolding right_total_def rel_fun_def
   apply (rule allI, rename_tac g)
   apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
   apply clarify
@@ -248,12 +248,12 @@
 
 lemma right_unique_fun [transfer_rule]:
   "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
-  unfolding right_total_def right_unique_def fun_rel_def
+  unfolding right_total_def right_unique_def rel_fun_def
   by (clarify, rule ext, fast)
 
 lemma bi_total_fun [transfer_rule]:
   "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
-  unfolding bi_total_def fun_rel_def
+  unfolding bi_total_def rel_fun_def
   apply safe
   apply (rename_tac f)
   apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
@@ -277,7 +277,7 @@
 
 lemma bi_unique_fun [transfer_rule]:
   "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
-  unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff
+  unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff
   by (safe, metis, fast)
 
 
@@ -288,7 +288,7 @@
   shows "((A ===> op =) ===> op =)
     (transfer_bforall (Domainp A)) transfer_forall"
   using assms unfolding right_total_def
-  unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
+  unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
   by metis
 
 text {* Transfer rules using implication instead of equality on booleans. *}
@@ -299,7 +299,7 @@
   "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
   "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
   "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
-  unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def
+  unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
   by metis+
 
 lemma transfer_implies_transfer [transfer_rule]:
@@ -312,7 +312,7 @@
   "(implies     ===> op =        ===> rev_implies) transfer_implies transfer_implies"
   "(op =        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
   "(op =        ===> op =        ===> rev_implies) transfer_implies transfer_implies"
-  unfolding transfer_implies_def rev_implies_def fun_rel_def by auto
+  unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
 
 lemma eq_imp_transfer [transfer_rule]:
   "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
@@ -321,42 +321,42 @@
 lemma eq_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(A ===> A ===> op =) (op =) (op =)"
-  using assms unfolding bi_unique_def fun_rel_def by auto
+  using assms unfolding bi_unique_def rel_fun_def by auto
 
 lemma right_total_Ex_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
-using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def]
+using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
 by blast
 
 lemma right_total_All_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
-using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def]
+using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
 by blast
 
 lemma All_transfer [transfer_rule]:
   assumes "bi_total A"
   shows "((A ===> op =) ===> op =) All All"
-  using assms unfolding bi_total_def fun_rel_def by fast
+  using assms unfolding bi_total_def rel_fun_def by fast
 
 lemma Ex_transfer [transfer_rule]:
   assumes "bi_total A"
   shows "((A ===> op =) ===> op =) Ex Ex"
-  using assms unfolding bi_total_def fun_rel_def by fast
+  using assms unfolding bi_total_def rel_fun_def by fast
 
 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma id_transfer [transfer_rule]: "(A ===> A) id id"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma comp_transfer [transfer_rule]:
   "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma fun_upd_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
@@ -365,11 +365,11 @@
 
 lemma case_nat_transfer [transfer_rule]:
   "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
-  unfolding fun_rel_def by (simp split: nat.split)
+  unfolding rel_fun_def by (simp split: nat.split)
 
 lemma rec_nat_transfer [transfer_rule]:
   "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
-  unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
+  unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
 
 lemma funpow_transfer [transfer_rule]:
   "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
@@ -409,7 +409,7 @@
   "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
-using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def 
+using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def 
 by fast+
 
 lemma right_unique_transfer [transfer_rule]:
@@ -417,7 +417,7 @@
   assumes [transfer_rule]: "right_total B"
   assumes [transfer_rule]: "bi_unique B"
   shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
-using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
+using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
 by metis
 
 end
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Word/Word.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -193,9 +193,9 @@
 text {* TODO: The next lemma could be generated automatically. *}
 
 lemma uint_transfer [transfer_rule]:
-  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
+  "(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a)))
     (uint :: 'a::len0 word \<Rightarrow> int)"
-  unfolding fun_rel_def word.pcr_cr_eq cr_word_def
+  unfolding rel_fun_def word.pcr_cr_eq cr_word_def
   by (simp add: no_bintr_alt1 uint_word_of_int)
 
 
@@ -651,9 +651,9 @@
 declare word_neg_numeral_alt [symmetric, code_abbrev]
 
 lemma word_numeral_transfer [transfer_rule]:
-  "(fun_rel op = pcr_word) numeral numeral"
-  "(fun_rel op = pcr_word) (- numeral) (- numeral)"
-  apply (simp_all add: fun_rel_def word.pcr_cr_eq cr_word_def)
+  "(rel_fun op = pcr_word) numeral numeral"
+  "(rel_fun op = pcr_word) (- numeral) (- numeral)"
+  apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
   using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
 
 lemma uint_bintrunc [simp]:
@@ -2295,9 +2295,9 @@
   by (simp add: word_ubin.eq_norm nth_bintr)
 
 lemma word_test_bit_transfer [transfer_rule]:
-  "(fun_rel pcr_word (fun_rel op = op =))
+  "(rel_fun pcr_word (rel_fun op = op =))
     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
-  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
+  unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
 
 lemma word_ops_nth_size:
   "n < size (x::'a::len0 word) \<Longrightarrow> 
diff -r 7ab8f003fe41 -r e96383acecf9 src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -37,79 +37,79 @@
   unfolding ZN_def by simp
 
 lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
-  unfolding fun_rel_def ZN_def by (simp add: int_mult)
+  unfolding rel_fun_def ZN_def by (simp add: int_mult)
 
 lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
-  unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
+  unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
 
 lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
-  unfolding fun_rel_def ZN_def by (simp add: int_power)
+  unfolding rel_fun_def ZN_def by (simp add: int_power)
 
 lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_All [transfer_rule]:
   "((ZN ===> op =) ===> op =) (Ball {0..}) All"
-  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
+  unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)
 
 lemma ZN_transfer_forall [transfer_rule]:
   "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
   unfolding transfer_forall_def transfer_bforall_def
-  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
+  unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)
 
 lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
-  unfolding fun_rel_def ZN_def Bex_def atLeast_iff
+  unfolding rel_fun_def ZN_def Bex_def atLeast_iff
   by (metis zero_le_imp_eq_int zero_zle_int)
 
 lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_numeral [transfer_rule]:
   "(op = ===> ZN) numeral numeral"
-  unfolding fun_rel_def ZN_def by simp
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
-  unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
+  unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
 
 lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
-  unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
+  unfolding rel_fun_def ZN_def by (simp add: zdiv_int)
 
 lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
-  unfolding fun_rel_def ZN_def by (simp add: zmod_int)
+  unfolding rel_fun_def ZN_def by (simp add: zmod_int)
 
 lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
-  unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
+  unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd)
 
 lemma ZN_atMost [transfer_rule]:
   "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
-  unfolding fun_rel_def ZN_def rel_set_def
+  unfolding rel_fun_def ZN_def rel_set_def
   by (clarsimp simp add: Bex_def, arith)
 
 lemma ZN_atLeastAtMost [transfer_rule]:
   "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
-  unfolding fun_rel_def ZN_def rel_set_def
+  unfolding rel_fun_def ZN_def rel_set_def
   by (clarsimp simp add: Bex_def, arith)
 
 lemma ZN_setsum [transfer_rule]:
   "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
-  apply (intro fun_relI)
+  apply (intro rel_funI)
   apply (erule (1) bi_unique_rel_set_lemma)
-  apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
+  apply (simp add: setsum.reindex int_setsum ZN_def rel_fun_def)
   apply (rule setsum_cong2, simp)
   done