# HG changeset patch
# User blanchet
# Date 1412244148 -7200
# Node ID cb68c3f564fe53c0173562bd39452d2ce1dac0a8
# Parent  ce0b9be06f85b41647fa66df5f6ec87b294c1cc7
fixed a few mistakes in the documentation

diff -r ce0b9be06f85 -r cb68c3f564fe src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Oct 02 12:02:27 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Oct 02 12:02:28 2014 +0200
@@ -653,9 +653,9 @@
 
 \noindent
 In addition, some of the plugins introduce their own constants
-(Section~\ref{sec:plugins}). The case combinator, discriminators, and selectors
-are collectively called \emph{destructors}. The prefix ``@{text "t."}'' is an
-optional component of the names and is normally hidden.
+(Section~\ref{sec:controlling-plugins}). The case combinator, discriminators,
+and selectors are collectively called \emph{destructors}. The prefix
+``@{text "t."}'' is an optional component of the names and is normally hidden.
 *}
 
 
@@ -685,9 +685,10 @@
 \noindent
 The full list of named theorems can be obtained as usual by entering the
 command \keyw{print_theorems} immediately after the datatype definition.
-This list includes theorems produced by plugins (Section~\ref{sec:plugins}),
-but normally excludes low-level theorems that reveal internal constructions. To
-make these accessible, add the line
+This list includes theorems produced by plugins
+(Section~\ref{sec:controlling-plugins}), but normally excludes low-level
+theorems that reveal internal constructions. To make these accessible, add
+the line
 *}
 
     declare [[bnf_note_all]]
@@ -2925,7 +2926,7 @@
 \end{indentblock}
 
 In addition, the plugin sets the @{text "[relator_eq_onp]"} attribute on a
-variant of the @{text t.rel_eq_onp} property generated by the @{text quotient}
+variant of the @{text t.rel_eq_onp} property generated by the @{text lifting}
 plugin, the @{text "[relator_mono]"} attribute on @{text t.rel_mono}, and the
 @{text "[relator_distr]"} attribute on @{text t.rel_compp}.
 *}