# HG changeset patch
# User paulson
# Date 853751927 -3600
# Node ID bc6e29c776d6e3044960d7a0bd3a0e91d0a74843
# Parent  0ba3755ce39800870f024a8e73d57dfec9703fd6
Documents the new command "prlim"

diff -r 0ba3755ce398 -r bc6e29c776d6 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Fri Jan 17 19:29:38 1997 +0100
+++ b/doc-src/Ref/goals.tex	Mon Jan 20 10:18:47 1997 +0100
@@ -250,10 +250,11 @@
 \begin{ttbox} 
 pr    : unit -> unit
 prlev : int -> unit
+prlim : int -> unit
 goals_limit: int ref \hfill{\bf initially 10}
 \end{ttbox}
-See also the printing control options described in
-\S\ref{sec:printing-control}. 
+See also the printing control options described 
+in~\S\ref{sec:printing-control}. 
 \begin{ttdescription}
 \item[\ttindexbold{pr}();] 
 prints the current proof state.
@@ -263,6 +264,11 @@
 of~$n$ refers to the $n$th previous level.  This command allows
 you to review earlier stages of the proof.
 
+\item[\ttindexbold{prlim} {\it k};] 
+prints the current proof state, limiting the number of subgoals to~$k$.  It
+updates {\tt goals_limit} (see below) and is helpful when there are many
+subgoals. 
+
 \item[\ttindexbold{goals_limit} := {\it k};] 
 specifies~$k$ as the maximum number of subgoals to print.
 \end{ttdescription}