diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index d73ab5d2c..c781c8274 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -211,7 +211,6 @@ backtracks one step. \begin{ErrMsgs} \item \errindex{No focused proof (No proof-editing in progress)} -\item \errindex{Undo stack would be exhausted} \end{ErrMsgs} \begin{Variants} @@ -222,18 +221,6 @@ backtracks one step. \end{Variants} -\subsection[\tt Set Undo {\num}.]{\tt Set Undo {\num}.\comindex{Set Undo}} - -This command changes the maximum number of {\tt Undo}'s that will be -possible when doing a proof. It only affects proofs started after -this command, such that if you want to change the current undo limit -inside a proof, you should first restart this proof. - -\subsection[\tt Unset Undo.]{\tt Unset Undo.\comindex{Unset Undo}} - -This command resets the default number of possible {\tt Undo} commands -(which is currently 12). - \subsection[\tt Restart.]{\tt Restart.\comindex{Restart}} This command restores the proof editing process to the original goal. |