src/HOL/Lifting.thy

--- a/src/HOL/Lifting.thy	Thu Apr 19 09:58:54 2012 +0200
+++ b/src/HOL/Lifting.thy	Thu Apr 19 08:45:13 2012 +0200
@@ -339,6 +339,9 @@
 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
 
+lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
+  using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
+
 end
 
 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}