NEWS
changeset 13541 44efea0e21fa
parent 13540 aede0306e214
child 13549 f1522b892a4c
     1.1 --- a/NEWS	Tue Aug 27 16:41:52 2002 +0200
     1.2 +++ b/NEWS	Tue Aug 27 17:24:41 2002 +0200
     1.3 @@ -22,11 +22,12 @@
     1.4  * Pure: improved thms_containing: proper indexing of facts instead of
     1.5  raw theorems; check validity of results wrt. current name space;
     1.6  include local facts of proof configuration (also covers active
     1.7 -locales); an optional limit for the number of printed facts may be
     1.8 -given (the default is 40);
     1.9 -
    1.10 -* Pure: disallow duplicate fact bindings within new-style theory
    1.11 -files;
    1.12 +locales), cover fixed variables in index; may use "_" in term
    1.13 +specification; an optional limit for the number of printed facts may
    1.14 +be given (the default is 40);
    1.15 +
    1.16 +* Pure: disallow duplicate fact bindings within new-style theory files
    1.17 +(batch-mode only);
    1.18  
    1.19  * Provers: improved induct method: assumptions introduced by case
    1.20  "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from