src/HOL/Lifting.thy
changeset 47575 b90cd7016d4f
parent 47545 a2850a16e30f
child 47651 8e4f50afd21a
     1.1 --- a/src/HOL/Lifting.thy	Thu Apr 19 09:58:54 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 19 08:45:13 2012 +0200
     1.3 @@ -339,6 +339,9 @@
     1.4  lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
     1.5    using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
     1.6  
     1.7 +lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
     1.8 +  using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
     1.9 +
    1.10  end
    1.11  
    1.12  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}