--- a/src/Doc/Prog_Prove/Logic.thy Tue Feb 24 19:57:51 2015 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Thu Feb 26 18:23:51 2015 +0100
@@ -188,7 +188,7 @@
\end{quote}
The key characteristics of both @{text simp} and @{text auto} are
\begin{itemize}
-\item They show you were they got stuck, giving you an idea how to continue.
+\item They show you where they got stuck, giving you an idea how to continue.
\item They perform the obvious steps but are highly incomplete.
\end{itemize}
A proof method is \conceptnoidx{complete} if it can prove all true formulas.