--- a/IntEx.thy	Thu Nov 12 02:54:40 2009 +0100
+++ b/IntEx.thy	Thu Nov 12 12:07:33 2009 +0100
@@ -134,6 +134,8 @@
   lift_thm lthy qty ty_name rsp_thms defs t
 *}
 
+print_quotients
+
 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
 lemma plus_assoc_pre: