--- a/doc-src/IsarRef/Thy/Misc.thy Sun Jan 29 22:12:25 2012 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Thu Feb 02 16:07:25 2012 +0100
@@ -114,35 +114,6 @@
*}
-section {* History commands \label{sec:history} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
- @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
- @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
- \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. 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 "linear_undo"}, or even @{command
- "kill"} commands would quickly result in utter confusion.
- \end{warn}
-*}
-
-
section {* System commands *}
text {*
--- a/doc-src/IsarRef/Thy/document/Misc.tex Sun Jan 29 22:12:25 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Thu Feb 02 16:07:25 2012 +0100
@@ -217,36 +217,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{History commands \label{sec:history}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ any{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{command}{linear\_undo}\hypertarget{command.linear-undo}{\hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isaliteral{5F}{\isacharunderscore}}undo}}}}}^{{ * }{ * }} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ any{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ any{\isaliteral{22}{\isachardoublequote}}} \\
- \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. 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{\isaliteral{5F}{\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.linear-undo}{\mbox{\isa{\isacommand{linear{\isaliteral{5F}{\isacharunderscore}}undo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} commands would quickly result in utter confusion.
- \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{System commands%
}
\isamarkuptrue%