1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 27 19:35:00 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 27 20:28:00 2011 +0200
     1.3 @@ -1236,6 +1236,52 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 +section {* Quotient types *}
     1.8 +
     1.9 +text {*
    1.10 +  The quotient package defines a new quotient type given a raw type
    1.11 +  and a partial equivalence relation.
    1.12 +  It also includes automation for transporting definitions and theorems.
    1.13 +  It can automatically produce definitions and theorems on the quotient type,
    1.14 +  given the corresponding constants and facts on the raw type.
    1.15 +
    1.16 +  \begin{matharray}{rcl}
    1.17 +    @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
    1.18 +    @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
    1.19 +    @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
    1.20 +    @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
    1.21 +    @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
    1.22 +  \end{matharray}
    1.23 +
    1.24 +  @{rail "
    1.25 +    @@{command (HOL) quotient_type} (spec + @'and');
    1.26 +
    1.27 +    spec: @{syntax typespec} @{syntax mixfix}? '=' \\
    1.28 +     @{syntax type} '/' ('partial' ':')? @{syntax term}; 
    1.29 +  "}
    1.30 +
    1.31 +  @{rail "
    1.32 +    @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
    1.33 +    @{syntax term} 'is' @{syntax term};
    1.34 + 
    1.35 +    constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
    1.36 +  "}
    1.37 +
    1.38 +  \begin{description}
    1.39 +  
    1.40 +  \item @{command (HOL) "quotient_type"} defines quotient types.
    1.41 +
    1.42 +  \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
    1.43 +
    1.44 +  \item @{command (HOL) "print_quotmaps"} prints quotient map functions.
    1.45 +
    1.46 +  \item @{command (HOL) "print_quotients"} prints quotients.
    1.47 +
    1.48 +  \item @{command (HOL) "print_quotconsts"} prints quotient constants.
    1.49 +
    1.50 +  \end{description}
    1.51 +
    1.52 +*}
    1.53  
    1.54  section {* Arithmetic proof support *}
    1.55