diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Oct 03 11:14:19 2011 +0200
@@ -159,7 +159,7 @@
   proof structure at all, but goes back right to the theory level.
   Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
   --- there is no intended claim to be able to complete the proof
-  anyhow.
+  in any way.
 
   A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
   \emph{within} the system itself, in conjunction with the document