'pr' now prints actual proof states only;
authorwenzelm
Thu May 18 17:21:58 2000 +0200 (2000-05-18)
changeset 88832a94bfd31285
parent 8882 9df44a4f1bf7
child 8884 d1c85d427e29
'pr' now prints actual proof states only;
doc-src/IsarRef/pure.tex
     1.1 --- a/doc-src/IsarRef/pure.tex	Thu May 18 11:43:57 2000 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Thu May 18 17:21:58 2000 +0200
     1.3 @@ -1136,11 +1136,10 @@
     1.4  \begin{descr}
     1.5  \item [$\isarkeyword{help}$] prints a list of available language elements.
     1.6    Note that methods and attributes depend on the current theory context.
     1.7 -\item [$\isarkeyword{pr}~n$] prints the current top-level state, i.e.\ the
     1.8 -  theory identifier or proof state.  The latter includes the proof context,
     1.9 -  current facts and goals.  The optional argument $n$ affects the implicit
    1.10 -  limit of goals to be displayed, which is initially 10.  Omitting the limit
    1.11 -  leaves the value unchanged.
    1.12 +\item [$\isarkeyword{pr}~n$] prints the current proof state (if present),
    1.13 +  including the proof context, current facts and goals.  The optional argument
    1.14 +  $n$ affects the implicit limit of goals to be displayed, which is initially
    1.15 +  10.  Omitting the limit leaves the current value unchanged.
    1.16  \item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory
    1.17    or proof context.  Note that any attributes included in the theorem
    1.18    specifications are applied to a temporary context derived from the current