src/Doc/Datatypes/Datatypes.thy

 
 \medskip
 
 \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.
 *}
 
 
 subsection {* Generated Theorems
   \label{ssec:datatype-generated-theorems} *}

 \end{itemize}
 
 \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]]
 (*<*)
     declare [[bnf_note_all = false]]

 
 \end{description}
 \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}.
 *}