# HG changeset patch
# User haftmann
# Date 1266930794 -3600
# Node ID f8bae261e7a982f3e61b34166a872eb567f49aa3
# Parent  cbdf785a1eb3e02c77e7b95009516be3a629c80e# Parent  c298a4fc324be0150c35dccf40688c305c6f6b48
merged

diff -r c298a4fc324b -r f8bae261e7a9 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Tue Feb 23 14:11:32 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Tue Feb 23 14:13:14 2010 +0100
@@ -37,7 +37,9 @@
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list
+  val rsp_rules_add: attribute
   val prs_rules_get: Proof.context -> thm list
+  val prs_rules_add: attribute
   val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
@@ -241,6 +243,7 @@
    val description = "Respectfulness theorems.")
 
 val rsp_rules_get = RspRules.get
+val rsp_rules_add = RspRules.add
 
 (* preservation theorems *)
 structure PrsRules = Named_Thms
@@ -248,6 +251,7 @@
    val description = "Preservation theorems.")
 
 val prs_rules_get = PrsRules.get
+val prs_rules_add = PrsRules.add
 
 (* id simplification theorems *)
 structure IdSimps = Named_Thms