--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 04 11:08:31 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 04 17:12:37 2012 +0200
@@ -115,6 +115,8 @@
[[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
|> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
+ |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
+ [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
| NONE => lthy
|> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
[quot_thm RS @{thm Quotient_All_transfer}])