1.1 --- a/doc-src/Nitpick/nitpick.tex	Sat Apr 24 16:33:01 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sat Apr 24 16:43:03 2010 +0200
     1.3 @@ -2498,25 +2498,6 @@
     1.4  Unless you are tracking down a bug in Nitpick or distrust the peephole
     1.5  optimizer, you should leave this option enabled.
     1.6  
     1.7 -\opdefault{sym\_break}{int}{20}
     1.8 -Specifies an upper bound on the number of relations for which Kodkod generates
     1.9 -symmetry breaking predicates. According to the Kodkod documentation
    1.10 -\cite{kodkod-2009-options}, ``in general, the higher this value, the more
    1.11 -symmetries will be broken, and the faster the formula will be solved. But,
    1.12 -setting the value too high may have the opposite effect and slow down the
    1.13 -solving.''
    1.14 -
    1.15 -\opdefault{sharing\_depth}{int}{3}
    1.16 -Specifies the depth to which Kodkod should check circuits for equivalence during
    1.17 -the translation to SAT. The default of 3 is the same as in Alloy. The minimum
    1.18 -allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
    1.19 -but can also slow down Kodkod.
    1.20 -
    1.21 -\opfalse{flatten\_props}{dont\_flatten\_props}
    1.22 -Specifies whether Kodkod should try to eliminate intermediate Boolean variables.
    1.23 -Although this might sound like a good idea, in practice it can drastically slow
    1.24 -down Kodkod.
    1.25 -
    1.26  \opdefault{max\_threads}{int}{0}
    1.27  Specifies the maximum number of threads to use in Kodkod. If this option is set
    1.28  to 0, Kodkod will compute an appropriate value based on the number of processor
    1.29 @@ -2569,7 +2550,7 @@
    1.30  Behind the scenes, Isabelle's built-in packages and theories rely on the
    1.31  following attributes to affect Nitpick's behavior:
    1.32  
    1.33 -\begin{itemize}
    1.34 +\begin{enum}
    1.35  \flushitem{\textit{nitpick\_def}}
    1.36  
    1.37  \nopagebreak
    1.38 @@ -2623,7 +2604,7 @@
    1.39  This attribute specifies the (free-form) specification of a constant defined
    1.40  using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
    1.41  
    1.42 -\end{itemize}
    1.43 +\end{enum}
    1.44  
    1.45  When faced with a constant, Nitpick proceeds as follows:
    1.46