src/Doc/Datatypes/Datatypes.thy

 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
 \item
 The @{text "plugins"} option indicates which plugins should be enabled
-(@{text only}) or disabled (@{text del}). Wildcards (``@{text "*"}'') are
-allowed (e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
+(@{text only}) or disabled (@{text del}). Some plugin names are defined
+as indirection to a group of sub-plugins (notably @{text "quickcheck"}
+based on @{text quickcheck_random}, @{text quickcheck_exhaustive}, \dots).
+By default, all plugins are enabled.
 
 \item
 The @{text "discs_sels"} option indicates that discriminators and selectors
 should be generated. The option is implicitly enabled if names are specified for
 discriminators or selectors.

 @{command codatatype}, @{command free_constructors}, @{command bnf}, and
 @{command bnf_axiomatization}.
 For example:
 *}
 
-    datatype (plugins del: code "quickcheck_*") color = Red | Black
+    datatype (plugins del: code "quickcheck") color = Red | Black
 
 
 subsection {* Code Generator
   \label{ssec:code-generator} *}