1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -544,9 +544,9 @@
     1.4  \prew
     1.5  \slshape
     1.6  The prover found a type-unsound proof involving ``\textit{foo}'',
     1.7 -``\textit{bar}'', ``\textit{baz}'' even though a supposedly type-sound encoding
     1.8 -was used (or, less likely, your axioms are inconsistent). You might want to
     1.9 -report this to the Isabelle developers.
    1.10 +``\textit{bar}'', and ``\textit{baz}'' even though a supposedly type-sound
    1.11 +encoding was used (or, less likely, your axioms are inconsistent). You might
    1.12 +want to report this to the Isabelle developers.
    1.13  \postw
    1.14  
    1.15  \point{Auto can solve it---why not Sledgehammer?}