--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 07:31:11 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 14:44:46 2011 +0100
@@ -1264,10 +1264,6 @@
(@'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};
@@ -1277,7 +1273,9 @@
\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.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 07:31:11 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 14:44:46 2011 +0100
@@ -1808,9 +1808,6 @@
\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}}}}}[]
@@ -1844,7 +1841,8 @@
\begin{description}
- \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types.
+ \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. 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.
\item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.