NEWS
changeset 9724 2030c5d63741
parent 9709 2d0ee9612ef1
child 9737 7aae235675dc
--- 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