author paulson Thu, 24 Oct 1996 11:41:43 +0200 changeset 2128 4e8644805af2 parent 2127 33f3d40145e8 child 2129 2ffe6e24f38d
Documents the use of negative arguments to choplev and prlev
 doc-src/Ref/goals.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/goals.tex	Thu Oct 24 10:43:38 1996 +0200
+++ b/doc-src/Ref/goals.tex	Thu Oct 24 11:41:43 1996 +0200
@@ -215,7 +215,9 @@
can cancel it.

\item[\ttindexbold{choplev} {\it n};]
-truncates the state list to level~{\it n}.
+truncates the state list to level~{\it n}, if $n\geq0$.  A negative value
+of~$n$ refers to the $n$th previous level:
+\hbox{\verb|choplev ~1|} has the same effect as {\tt chop}.

\item[\ttindexbold{back}();]
searches the state list for a non-empty branch point, starting from the top
@@ -257,8 +259,9 @@
prints the current proof state.

\item[\ttindexbold{prlev} {\it n};]
-prints the proof state at level {\it n}.  This allows you to review the
-previous steps of the proof.
+prints the proof state at level {\it n}, if $n\geq0$.  A negative value
+of~$n$ refers to the $n$th previous level.  This command allows
+you to review earlier stages of the proof.

\item[\ttindexbold{goals_limit} := {\it k};]
specifies~$k$ as the maximum number of subgoals to print.