src/HOL/Lifting.thy
changeset 47889 29212a4bb866
parent 47777 f29e7dcd7c40
child 47936 756f30eac792
     1.1 --- a/src/HOL/Lifting.thy	Fri May 04 11:08:31 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Fri May 04 17:12:37 2012 +0200
     1.3 @@ -310,6 +310,9 @@
     1.4  lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
     1.5    using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
     1.6  
     1.7 +lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
     1.8 +  using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
     1.9 +
    1.10  end
    1.11  
    1.12  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}