diff -r 2e51e1315839 -r 520a4084d064 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 17:30:00 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 prs_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
@@ -180,7 +181,7 @@
 
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
-  (val name = "quotient_equiv"
+  (val name = "quot_equiv"
    val description = "Equivalence relation theorems.")
 
 val equiv_rules_get = EquivRules.get
@@ -188,11 +189,18 @@
 
 (* respectfulness theorems *)
 structure RspRules = Named_Thms
-  (val name = "quotient_rsp"
+  (val name = "quot_respect"
    val description = "Respectfulness theorems.")
 
 val rsp_rules_get = RspRules.get
 
+(* preservation theorems *)
+structure PrsRules = Named_Thms
+  (val name = "quot_preserve"
+   val description = "Respectfulness theorems.")
+
+val prs_rules_get = PrsRules.get
+
 (* respectfulness theorems *)
 structure IdSimps = Named_Thms
   (val name = "id_simps"
@@ -202,7 +210,7 @@
 
 (* quotient theorems *)
 structure QuotientRules = Named_Thms
-  (val name = "quotient_thm"
+  (val name = "quot_thm"
    val description = "Quotient theorems.")
 
 val quotient_rules_get = QuotientRules.get