--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 10 09:02:51 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 10 09:47:59 2012 +0100
@@ -1272,6 +1272,7 @@
@{method_def (HOL) "regularize"} & : & @{text method} \\
@{method_def (HOL) "injection"} & : & @{text method} \\
@{method_def (HOL) "cleaning"} & : & @{text method} \\
+ @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\
@{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
@{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
@{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
@@ -1366,6 +1367,17 @@
local theory store and used by the @{method (HOL) "injection"}
and @{method (HOL) "cleaning"} methods respectively.
+ \item @{attribute (HOL) quot_thm} declares that a certain theorem
+ is a quotient extension theorem. Quotient extension theorems
+ allow for quotienting inside container types. Given a polymorphic
+ type that serves as a container, a map function defined for this
+ container using @{command (HOL) "enriched_type"} and a relation
+ map defined for for the container type, the quotient extension
+ theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
+ (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
+ are stored in a database and are used all the steps of lifting
+ theorems.
+
\end{description}
*}