Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorhaftmann
Tue, 23 Feb 2010 14:13:14 +0100
changeset 35322 f8bae261e7a9
parent 35314 cbdf785a1eb3 (diff)
parent 35321 c298a4fc324b (current diff)
child 35323 259931828ecc
merged
src/HOL/Hoare/HoareAbort.thy file | annotate | diff | comparison | revisions
src/HOL/W0/README.html file | annotate | diff | comparison | revisions
src/HOL/W0/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/W0/W0.thy file | annotate | diff | comparison | revisions
src/HOL/W0/document/root.tex file | annotate | diff | comparison | revisions 
--- 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
isabelle