# HG changeset patch
# User wenzelm
# Date 1216112354 -7200
# Node ID b66e257b75f53e3c6c941ebb93d9ffdb91cb1354
# Parent  beb9b5f07dbc4916c1e86045247d00acb4ea337d
removed command 'redo';
added command 'linear_undo';

diff -r beb9b5f07dbc -r b66e257b75f5 doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Tue Jul 15 10:49:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/Misc.thy	Tue Jul 15 10:59:14 2008 +0200
@@ -191,25 +191,26 @@
 text {*
   \begin{matharray}{rcl}
     @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
-    @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+    @{command_def "linear_undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
     @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   \end{matharray}
 
   The Isabelle/Isar top-level maintains a two-stage history, for
   theory and proof state transformation.  Basically, any command can
   be undone using @{command "undo"}, excluding mere diagnostic
-  elements.  Its effect may be revoked via @{command "redo"}, unless
-  the corresponding @{command "undo"} step has crossed the beginning
-  of a proof or theory.  The @{command "kill"} command aborts the
-  current history node altogether, discontinuing a proof or even the
-  whole theory.  This operation is \emph{not} undo-able.
+  elements.  Note that a theorem statement with a \emph{finished}
+  proof is treated as a single unit by @{command "undo"}.  In
+  contrast, the variant @{command "linear_undo"} admits to step back
+  into the middle of a proof.  The @{command "kill"} command aborts
+  the current history node altogether, discontinuing a proof or even
+  the whole theory.  This operation is \emph{not} undo-able.
 
   \begin{warn}
     History commands should never be used with user interfaces such as
     Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
     care of stepping forth and back itself.  Interfering by manual
-    @{command "undo"}, @{command "redo"}, or even @{command "kill"}
-    commands would quickly result in utter confusion.
+    @{command "undo"}, @{command "linear_undo"}, or even @{command
+    "kill"} commands would quickly result in utter confusion.
   \end{warn}
 *}
 
diff -r beb9b5f07dbc -r b66e257b75f5 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Tue Jul 15 10:49:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Tue Jul 15 10:59:14 2008 +0200
@@ -212,25 +212,25 @@
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
     \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
-    \indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+    \indexdef{}{command}{linear\_undo}\hypertarget{command.linear-undo}{\hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
     \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   \end{matharray}
 
   The Isabelle/Isar top-level maintains a two-stage history, for
   theory and proof state transformation.  Basically, any command can
   be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic
-  elements.  Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless
-  the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning
-  of a proof or theory.  The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the
-  current history node altogether, discontinuing a proof or even the
-  whole theory.  This operation is \emph{not} undo-able.
+  elements.  Note that a theorem statement with a \emph{finished}
+  proof is treated as a single unit by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.  In
+  contrast, the variant \hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}} admits to step back
+  into the middle of a proof.  The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts
+  the current history node altogether, discontinuing a proof or even
+  the whole theory.  This operation is \emph{not} undo-able.
 
   \begin{warn}
     History commands should never be used with user interfaces such as
     Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
     care of stepping forth and back itself.  Interfering by manual
-    \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}
-    commands would quickly result in utter confusion.
+    \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} commands would quickly result in utter confusion.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%