1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Nov 29 18:22:31 2011 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Nov 29 15:52:51 2011 +0100
     1.3 @@ -1260,9 +1260,14 @@
     1.4      @@{command (HOL) quotient_type} (spec + @'and');
     1.5  
     1.6      spec: @{syntax typespec} @{syntax mixfix}? '=' \\
     1.7 -     @{syntax type} '/' ('partial' ':')? @{syntax term}; 
     1.8 +     @{syntax type} '/' ('partial' ':')? @{syntax term} \\
     1.9 +     (@'morphisms' @{syntax name} @{syntax name})?; 
    1.10    "}
    1.11  
    1.12 + The injection from a quotient type to a raw type is called @{text rep_t},
    1.13 +  its inverse @{text abs_t} unless explicit @{keyword (HOL)
    1.14 +  "morphisms"} specification provides alternative names.
    1.15 +
    1.16    @{rail "
    1.17      @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
    1.18      @{syntax term} 'is' @{syntax term};

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Nov 29 18:22:31 2011 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Nov 29 15:52:51 2011 +0100
     2.3 @@ -1785,7 +1785,7 @@
     2.4  \rail@cterm{\isa{\isakeyword{and}}}[]
     2.5  \rail@endplus
     2.6  \rail@end
     2.7 -\rail@begin{5}{\isa{spec}}
     2.8 +\rail@begin{8}{\isa{spec}}
     2.9  \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
    2.10  \rail@bar
    2.11  \rail@nextbar{1}
    2.12 @@ -1801,10 +1801,20 @@
    2.13  \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
    2.14  \rail@endbar
    2.15  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    2.16 +\rail@cr{6}
    2.17 +\rail@bar
    2.18 +\rail@nextbar{7}
    2.19 +\rail@term{\isa{\isakeyword{morphisms}}}[]
    2.20 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    2.21 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    2.22 +\rail@endbar
    2.23  \rail@end
    2.24  \end{railoutput}
    2.25  
    2.26  
    2.27 + The injection from a quotient type to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t},
    2.28 +  its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
    2.29 +
    2.30    \begin{railoutput}
    2.31  \rail@begin{4}{}
    2.32  \rail@term{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[]