# HG changeset patch
# User blanchet
# Date 1305888478 -7200
# Node ID d7447b8c42657ffd23596999d9db9f4a8d7aa0ac
# Parent  e336ef6313aa1e4921c4cdc328445b8e03a9357d
updated FAQ

diff -r e336ef6313aa -r d7447b8c4265 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 20 12:47:58 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 20 12:47:58 2011 +0200
@@ -439,9 +439,10 @@
 
 \begin{quote}
 \slshape
-The prover found a type-unsound proof even though a supposedly type-sound
-encoding was used (or, very unlikely, your axioms are inconsistent). You
-might want to report this to the Isabelle developers.
+The prover found a type-unsound proof involving ``\textit{foo}'',
+``\textit{bar}'', ``\textit{baz}'' even though a supposedly type-sound encoding
+was used (or, less likely, your axioms are inconsistent). You might want to
+report this to the Isabelle developers.
 \end{quote}
 
 \point{Auto can solve it---why not Sledgehammer?}