--- 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