src/HOL/Lifting.thy
changeset 71262 a30278c8585f
parent 69913 ca515cf61651
child 80672 28e8d402a9ba
--- 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