# HG changeset patch # User nipkow # Date 1424971431 -3600 # Node ID 8cd6fba08a90cc9ab25c96e15a8143cd2946ba1a # Parent 3ff1dd7ac7f090ba44fb171d82d1b05ee99841e1 typo 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.