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