# HG changeset patch
# User blanchet
# Date 1394788652 -3600
# Node ID 315cc3c0a19ac45f53d5ff1ee8317e2f682ce472
# Parent  a27859b0ef7d42850f05ffc95bc124e913d6aa0a
tuned wording (pun)

diff -r a27859b0ef7d -r 315cc3c0a19a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Mar 14 10:08:33 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Mar 14 10:17:32 2014 +0100
@@ -481,7 +481,8 @@
 The syntactic entity \synt{target} can be used to specify a local
 context---e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}.
 
-The optional target is potentially followed by datatype-specific options:
+The optional target is optionally followed by one or both of the following
+options:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
@@ -1383,7 +1384,7 @@
 \synt{thmdecl} denotes an optional name for the formula that follows, and
 \synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
 
-The optional target is potentially followed by a recursion-specific option:
+The optional target is optionally followed by the following option:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
@@ -1829,8 +1830,8 @@
 
 text {*
 \noindent
-Constructs such as @{text "let"}---@{text "in"}, @{text
-"if"}---@{text "then"}---@{text "else"}, and @{text "case"}---@{text "of"} may
+Constructs such as @{text "let"}--@{text "in"}, @{text
+"if"}--@{text "then"}--@{text "else"}, and @{text "case"}--@{text "of"} may
 appear around constructors that guard corecursive calls:
 *}
 
@@ -2280,7 +2281,8 @@
 \synt{thmdecl} denotes an optional name for the formula that follows, and
 \synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
 
-The optional target is potentially followed by a corecursion-specific option:
+The optional target is optionally followed by one or both of the following
+options:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}