# HG changeset patch
# User kuncar
# Date 1323092686 -3600
# Node ID fe2fd2f76f48642d5ca9b1be8180689f33c8013b
# Parent  b5db02fa9536b1cf2650a6a865f8a32b03c0be3a
the note about morphisms moved in the description part

diff -r b5db02fa9536 -r fe2fd2f76f48 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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.
 
diff -r b5db02fa9536 -r fe2fd2f76f48 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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.