doc-src/Nitpick/nitpick.tex
changeset 36126 00d550b6cfd4
parent 35811 3939ca38f366
child 36268 65aabc2c89ae
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Apr 13 11:13:52 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Apr 13 11:43:11 2010 +0200
     1.3 @@ -1445,8 +1445,8 @@
     1.4      (\!\begin{aligned}[t]%
     1.5      & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
     1.6      & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
     1.7 -The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
     1.8 -even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
     1.9 +The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
    1.10 +be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
    1.11  \postw
    1.12  
    1.13  Reading the Nitpick manual is a most excellent idea.