src/HOL/Lifting.thy
changeset 57398 882091eb1e9a
parent 56524 f4ba736040fa
child 57961 10b2f60b70f0
     1.1 --- a/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4  
     1.5  lemma Quotient_alt_def5:
     1.6    "Quotient R Abs Rep T \<longleftrightarrow>
     1.7 -    T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
     1.8 +    T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
     1.9    unfolding Quotient_alt_def4 Grp_def by blast
    1.10  
    1.11  lemma fun_quotient: