summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 18 May 2000 17:21:58 +0200 | |

changeset 8883 | 2a94bfd31285 |

parent 8882 | 9df44a4f1bf7 |

child 8884 | d1c85d427e29 |

'pr' now prints actual proof states only;

--- 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