src/HOL/Lifting.thy

     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
   unfolding Quotient_alt_def3 fun_eq_iff by auto
 
 lemma Quotient_alt_def5:
   "Quotient R Abs Rep T \<longleftrightarrow>
-    T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
+    T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
   unfolding Quotient_alt_def4 Grp_def by blast
 
 lemma fun_quotient:
   assumes 1: "Quotient R1 abs1 rep1 T1"
   assumes 2: "Quotient R2 abs2 rep2 T2"