# HG changeset patch
# User wenzelm
# Date 967572602 -7200
# Node ID 2030c5d6374189f7747d2c333d8d3baf1eb4fbbc
# Parent  a977245dfc8a24445856884088eb2b4cd3cc2ecf
* 'pr' command: optional argument for ProofContext.prems_limit;

diff -r a977245dfc8a -r 2030c5d63741 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