# HG changeset patch
# User kuncar
# Date 1323092821 -3600
# Node ID 97be233b32ed8e1e16a9bc9e8c52ea01b6e1f412
# Parent  fe2fd2f76f48642d5ca9b1be8180689f33c8013b# Parent  46046d8e96590de7d6149893c3a7e97a995b7029
merged

diff -r 46046d8e9659 -r 97be233b32ed doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 05 12:36:28 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 05 14:47:01 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 46046d8e9659 -r 97be233b32ed doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 05 12:36:28 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 05 14:47:01 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.