# HG changeset patch
# User kuncar
# Date 1322578371 -3600
# Node ID 1a6206f538d44ef646c9e29b0f6bbbfebd28d373
# Parent  af0b0e628e51c8bc3785dcbcdc87432ddb7b36f1
updated documentation for the quotient package

diff -r af0b0e628e51 -r 1a6206f538d4 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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};
diff -r af0b0e628e51 -r 1a6206f538d4 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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}}}}}[]