doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 46448 f1201fac7398
parent 46447 f37da60a8cc6
child 46457 915af80f74b3
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 10 09:02:51 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 10 09:47:59 2012 +0100
     1.3 @@ -1272,6 +1272,7 @@
     1.4      @{method_def (HOL) "regularize"} & : & @{text method} \\
     1.5      @{method_def (HOL) "injection"} & : & @{text method} \\
     1.6      @{method_def (HOL) "cleaning"} & : & @{text method} \\
     1.7 +    @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\
     1.8      @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
     1.9      @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
    1.10      @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
    1.11 @@ -1366,6 +1367,17 @@
    1.12      local theory store and used by the @{method (HOL) "injection"}
    1.13      and @{method (HOL) "cleaning"} methods respectively.
    1.14  
    1.15 +  \item @{attribute (HOL) quot_thm} declares that a certain theorem
    1.16 +    is a quotient extension theorem. Quotient extension theorems
    1.17 +    allow for quotienting inside container types. Given a polymorphic
    1.18 +    type that serves as a container, a map function defined for this
    1.19 +    container  using @{command (HOL) "enriched_type"} and a relation
    1.20 +    map defined for for the container type, the quotient extension
    1.21 +    theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
    1.22 +    (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
    1.23 +    are stored in a database and are used all the steps of lifting
    1.24 +    theorems.
    1.25 +
    1.26    \end{description}
    1.27  
    1.28  *}