doc-src/IsarRef/Thy/HOL_Specific.thy

     spec: @{syntax typespec} @{syntax mixfix}? '=' \\
      @{syntax type} '/' ('partial' ':')? @{syntax term} \\
      (@'morphisms' @{syntax name} @{syntax name})?; 
   "}
 
- The injection from a quotient type to a raw type is called @{text rep_t},
-  its inverse @{text abs_t} unless explicit @{keyword (HOL)
-  "morphisms"} specification provides alternative names.
-
   @{rail "
     @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
     @{syntax term} 'is' @{syntax term};
  
     constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
   "}
 
   \begin{description}
   
-  \item @{command (HOL) "quotient_type"} defines quotient types.
+  \item @{command (HOL) "quotient_type"} defines quotient types. The injection from a quotient type 
+  to a raw type is called @{text rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
+  "morphisms"} specification provides alternative names.
 
   \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
 
   \item @{command (HOL) "print_quotmaps"} prints quotient map functions.