author | wenzelm |

Thu May 18 17:21:58 2000 +0200 (2000-05-18) | |

changeset 8883 | 2a94bfd31285 |

parent 8882 | 9df44a4f1bf7 |

child 8884 | d1c85d427e29 |

'pr' now prints actual proof states only;

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