--- 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}}}}}[]