--- 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}.
*}