# HG changeset patch
# User wenzelm
# Date 958663318 -7200
# Node ID 2a94bfd31285cfd504ca163b5531a4fc1f9e061e
# Parent  9df44a4f1bf7f064fa9c3a9099a7879fad0db42f
'pr' now prints actual proof states only;

diff -r 9df44a4f1bf7 -r 2a94bfd31285 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu May 18 11:43:57 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Thu May 18 17:21:58 2000 +0200
@@ -1136,11 +1136,10 @@
 \begin{descr}
 \item [$\isarkeyword{help}$] prints a list of available language elements.
   Note that methods and attributes depend on the current theory context.
-\item [$\isarkeyword{pr}~n$] prints the current top-level state, i.e.\ the
-  theory identifier or proof state.  The latter includes the proof context,
-  current facts and goals.  The optional argument $n$ affects the implicit
-  limit of goals to be displayed, which is initially 10.  Omitting the limit
-  leaves the value unchanged.
+\item [$\isarkeyword{pr}~n$] prints the current proof state (if present),
+  including the proof context, current facts and goals.  The optional argument
+  $n$ affects the implicit limit of goals to be displayed, which is initially
+  10.  Omitting the limit leaves the current value unchanged.
 \item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory
   or proof context.  Note that any attributes included in the theorem
   specifications are applied to a temporary context derived from the current