doc-src/IsarRef/Thy/document/Proof.tex

   \emph{within} the system itself, in conjunction with the document
   preparation tools of Isabelle described in \chref{ch:document-prep}.
   Thus partial or even wrong proof attempts can be discussed in a
   logically sound manner.  Note that the Isabelle {\LaTeX} macros can
   be easily adapted to print something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' instead of
-  the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.
-
-  \medskip The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command is undo-able, unlike
-  \indexref{}{command}{kill}\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} (see \secref{sec:history}).  The effect is to
-  get back to the theory just before the opening of the proof.%
+  the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Statements%
 }