diff -r 3ff1dd7ac7f0 -r 8cd6fba08a90 src/Doc/Prog_Prove/Logic.thy
--- 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.