# HG changeset patch
# User blanchet
# Date 1307390638 -7200
# Node ID 37d507be30143dbce9cbab7e142bb164e2294e9a
# Parent  7b89836fd607e3f6053705c14908abff37cca17f
minor: curly brackets, not square brackets

diff -r 7b89836fd607 -r 37d507be3014 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Jun 06 21:58:29 2011 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Mon Jun 06 22:03:58 2011 +0200
@@ -1905,9 +1905,9 @@
 \item[$\bullet$] \qtybf{type}: A HOL type.
 \end{enum}
 
-Default values are indicated in square brackets. Boolean options have a negated
-counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
-Boolean options, ``= \textit{true}'' may be omitted.
+Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
+have a negated counterpart (e.g., \textit{blocking} vs.\
+\textit{non\_blocking}). When setting them, ``= \textit{true}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}
diff -r 7b89836fd607 -r 37d507be3014 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 21:58:29 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 22:03:58 2011 +0200
@@ -707,9 +707,9 @@
 seconds).
 \end{enum}
 
-Default values are indicated in braces. Boolean options have a negated
-counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
-Boolean options, ``= \textit{true}'' may be omitted.
+Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
+have a negated counterpart (e.g., \textit{blocking} vs.\
+\textit{non\_blocking}). When setting them, ``= \textit{true}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}