--- a/Quot/QuotMain.thy	Thu Feb 04 18:09:20 2010 +0100
+++ b/Quot/QuotMain.thy	Fri Feb 05 10:45:49 2010 +0100
@@ -150,7 +150,6 @@
 text {* Tactics for proving the lifted theorems *}
 use "quotient_tacs.ML"
 
-
 section {* Methods / Interface *}
 
 ML {*
@@ -181,5 +180,9 @@
   {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
   {* Proves automatically the cleaning goals from the lifting procedure. *}
 
+attribute_setup quot_lifted =
+  {* Scan.succeed Quotient_Tacs.lifted_attr *}
+  {* Lifting of theorems to quotient types. *}
+
 end