# HG changeset patch
# User blanchet
# Date 1410196874 -7200
# Node ID 8f91d42da3083efd0b27da4102cc07184874854e
# Parent  265aea1e9985f109ee2812867778c64694ff0383
compile

diff -r 265aea1e9985 -r 8f91d42da308 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 19:21:07 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 19:21:14 2014 +0200
@@ -507,8 +507,8 @@
 
 \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}). Wildcards (``@{text "*"}'') are
+allowed (e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
 
 \item
 The @{text "discs_sels"} option indicates that discriminators and selectors