src/HOL/Lifting.thy
changeset 47351 0193e663a19e
parent 47325 ec6187036495
child 47354 95846613e414
     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 04 13:41:38 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 04 13:42:01 2012 +0200
     1.3 @@ -273,6 +273,11 @@
     1.4    show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
     1.5  qed
     1.6  
     1.7 +lemma Quotient_to_transfer:
     1.8 +  assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
     1.9 +  shows "T c c'"
    1.10 +  using assms by (auto dest: Quotient_cr_rel)
    1.11 +
    1.12  subsection {* ML setup *}
    1.13  
    1.14  text {* Auxiliary data for the lifting package *}