# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266930706 -3600
# Node ID cbdf785a1eb3e02c77e7b95009516be3a629c80e
# Parent  956d08ec5d6569df3c30260a4c1f8b18cb92e11e
export prs_rules and rsp_rules attributes

diff -r 956d08ec5d65 -r cbdf785a1eb3 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Tue Feb 23 12:14:46 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Tue Feb 23 14:11:46 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