--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Sep 06 22:08:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Sep 06 22:31:54 2010 +0200
@@ -55,7 +55,7 @@
;
( 'prf' | 'full\_prf' ) modes? thmrefs?
;
- 'pr' modes? nat? (',' nat)?
+ 'pr' modes? nat?
;
modes: '(' (name + ) ')'
@@ -90,11 +90,11 @@
compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
there.
- \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} 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 \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} prints the current proof state
+ (if present), including current facts and goals. The optional limit
+ arguments affect the number of goals to be displayed, which is
+ initially 10. Omitting limit value leaves the current setting
+ unchanged.
\end{description}