* 'pr' command: optional argument for ProofContext.prems_limit;
authorwenzelm
Tue, 29 Aug 2000 20:10:02 +0200
changeset 9724 2030c5d63741
parent 9723 a977245dfc8a
child 9725 d53e4fd36448
* 'pr' command: optional argument for ProofContext.prems_limit;
NEWS
--- a/NEWS	Tue Aug 29 16:05:13 2000 +0200
+++ b/NEWS	Tue Aug 29 20:10:02 2000 +0200
@@ -191,8 +191,9 @@
 
 * names of theorems etc. may be natural numbers as well;
 
-* 'pr' command: optional goals_limit argument; no longer prints theory
-contexts, but only proof states;
+* 'pr' command: optional arguments for goals_limit and
+ProofContext.prems_limit; no longer prints theory contexts, but only
+proof states;
 
 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
 additional print modes to be specified; e.g. "pr(latex)" will print