--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Nov 29 18:22:31 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Nov 29 15:52:51 2011 +0100
@@ -1260,9 +1260,14 @@
@@{command (HOL) quotient_type} (spec + @'and');
spec: @{syntax typespec} @{syntax mixfix}? '=' \\
- @{syntax type} '/' ('partial' ':')? @{syntax term};
+ @{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};
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 29 18:22:31 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 29 15:52:51 2011 +0100
@@ -1785,7 +1785,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{5}{\isa{spec}}
+\rail@begin{8}{\isa{spec}}
\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1801,10 +1801,20 @@
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@cr{6}
+\rail@bar
+\rail@nextbar{7}
+\rail@term{\isa{\isakeyword{morphisms}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@endbar
\rail@end
\end{railoutput}
+ The injection from a quotient type to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t},
+ its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
+
\begin{railoutput}
\rail@begin{4}{}
\rail@term{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[]