# HG changeset patch
# User wenzelm
# Date 1030461881 -7200
# Node ID 44efea0e21fa54bd54087f6c71e3479288869a26
# Parent  aede0306e21400e18c9a004f7daccbe27e0c357d
*** empty log message ***

diff -r aede0306e214 -r 44efea0e21fa NEWS
--- a/NEWS	Tue Aug 27 16:41:52 2002 +0200
+++ b/NEWS	Tue Aug 27 17:24:41 2002 +0200
@@ -22,11 +22,12 @@
 * Pure: improved thms_containing: proper indexing of facts instead of
 raw theorems; check validity of results wrt. current name space;
 include local facts of proof configuration (also covers active
-locales); an optional limit for the number of printed facts may be
-given (the default is 40);
-
-* Pure: disallow duplicate fact bindings within new-style theory
-files;
+locales), cover fixed variables in index; may use "_" in term
+specification; an optional limit for the number of printed facts may
+be given (the default is 40);
+
+* Pure: disallow duplicate fact bindings within new-style theory files
+(batch-mode only);
 
 * Provers: improved induct method: assumptions introduced by case
 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from