# HG changeset patch
# User wenzelm
# Date 967572724 -7200
# Node ID 5e18de753e0f52140e1f3dd992f603603828a5d3
# Parent  78f9bcd9585e85728208a636185fe286aab2feb4
'syntax': improved mode spec;
'pr': prems limit;

diff -r 78f9bcd9585e -r 5e18de753e0f doc-src/IsarRef/pure.tex
--- 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.