diff -r 4765fec43414 -r a30278c8585f src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Tue Dec 10 01:06:39 2019 +0100 +++ b/src/HOL/Lifting.thy Tue Dec 10 01:06:39 2019 +0100 @@ -545,7 +545,7 @@ end (* needed for lifting_def_code_dt.ML (moved from Lifting_Set) *) -lemma right_total_UNIV_transfer: +lemma right_total_UNIV_transfer: assumes "right_total A" shows "(rel_set A) (Collect (Domainp A)) UNIV" using assms unfolding right_total_def rel_set_def Domainp_iff by blast