src/HOL/Lifting.thy
changeset 57398 882091eb1e9a
parent 56524 f4ba736040fa
child 57961 10b2f60b70f0
--- a/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -163,7 +163,7 @@
 
 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: