1.1 --- a/doc-src/IsarRef/Thy/Proof.thy Thu Sep 29 09:37:59 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Oct 03 11:14:19 2011 +0200
1.3 @@ -129,7 +129,7 @@
1.4 proof structure at all, but goes back right to the theory level.
1.5 Furthermore, @{command "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 @{command "oops"} is to explain Isar proofs
1.11 \emph{within} the system itself, in conjunction with the document