changeset 55610 | 9066b603dff6 |
parent 55604 | 42e4e8c2e8dc |
child 55731 | 66df76dd2640 |
--- a/src/HOL/Lifting.thy Thu Feb 20 16:56:32 2014 +0100 +++ b/src/HOL/Lifting.thy Thu Feb 20 16:56:33 2014 +0100 @@ -155,6 +155,10 @@ using a unfolding Quotient_def by blast +lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t" + using a unfolding Quotient_def + by blast + lemma Quotient_rep_abs_fold_unmap: assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" shows "R (Rep' x') x"