diff -r 9be4d8c8d842 -r f21c8ecbf8d5 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Thu Feb 02 16:38:15 2012 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Feb 02 17:52:16 2012 +0100
@@ -138,10 +138,6 @@
   logically sound manner.  Note that the Isabelle {\LaTeX} macros can
   be easily adapted to print something like ``@{text "\<dots>"}'' instead of
   the keyword ``@{command "oops"}''.
-
-  \medskip The @{command "oops"} command is undo-able, unlike
-  @{command_ref "kill"} (see \secref{sec:history}).  The effect is to
-  get back to the theory just before the opening of the proof.
 *}