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