--- 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.
*}
--- a/doc-src/IsarRef/Thy/document/Proof.tex Thu Feb 02 16:38:15 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Thu Feb 02 17:52:16 2012 +0100
@@ -167,11 +167,7 @@
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%
%