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

author | wenzelm |

Tue, 29 Aug 2000 20:12:04 +0200 | |

changeset 9727 | 5e18de753e0f |

parent 9726 | 78f9bcd9585e |

child 9728 | 1546ad1c7839 |

'syntax': improved mode spec;
'pr': prems limit;

--- a/doc-src/IsarRef/pure.tex Tue Aug 29 20:11:11 2000 +0200 +++ b/doc-src/IsarRef/pure.tex Tue Aug 29 20:12:04 2000 +0200 @@ -268,7 +268,7 @@ \end{matharray} \begin{rail} - 'syntax' ('(' name 'output'? ')')? (constdecl +) + 'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +) ; 'translations' (transpat ('==' | '=>' | '<=') transpat comment? +) ; @@ -1155,7 +1155,7 @@ does not apply here, the theory or proof configuration is not changed. \begin{rail} - 'pr' modes? nat? + 'pr' modes? nat? (',' nat)? ; 'thm' modes? thmrefs ; @@ -1171,17 +1171,18 @@ \end{rail} \begin{descr} -\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{pr}~goals, prems$] prints the current proof state (if + present), including the proof context, current facts and goals. The + optional limit arguments affect the number of goals and premises to be + displayed, which is initially 10 for both. Omitting limit values leaves the + current setting 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 theory or proof; the result is discarded, i.e.\ attributes involved in $\vec a$ do not have any permanent effect. -\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and - print terms or propositions according to the current theory or proof +\item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, type-check + and print terms or propositions according to the current theory or proof context; the inferred type of $t$ is output as well. Note that these commands are also useful in inspecting the current environment of term abbreviations.