# HG changeset patch
# User wenzelm
# Date 1328201536 -3600
# Node ID f21c8ecbf8d5e04984955e4e0f0ab360f7e83469
# Parent  9be4d8c8d84270424b64f527bace2e1bb72f5fae
discontinued obscure history commands;

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.
 *}
 
 
diff -r 9be4d8c8d842 -r f21c8ecbf8d5 doc-src/IsarRef/Thy/document/Proof.tex
--- 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%
 %