--- a/Quot/quotient_info.ML	Tue Dec 08 01:00:21 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 01:25:43 2009 +0100
@@ -26,6 +26,7 @@
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list  
+  val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
 end;
@@ -174,6 +175,9 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
+(* FIXME/TODO: check the various lemmas conform *)
+(* with the required shape                      *)
+
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
   (val name = "quotient_equiv"
@@ -189,6 +193,13 @@
 
 val rsp_rules_get = RspRules.get
 
+(* respectfulness theorems *)
+structure IdSimps = Named_Thms
+  (val name = "id_simps"
+   val description = "Identity simp rules for maps.")
+
+val id_simps_get = IdSimps.get
+
 (* quotient theorems *)
 structure QuotientRules = Named_Thms
   (val name = "quotient_thm"
@@ -201,6 +212,7 @@
 val _ = Context.>> (Context.map_theory 
     (EquivRules.setup #>
      RspRules.setup #>
+     IdSimps.setup #>
      QuotientRules.setup))
 
 end; (* structure *)