NEWS
changeset 23379 d0e3f790bd73
parent 23377 197b6a39592c
child 23449 dd874e6a3282
     1.1 --- a/NEWS	Thu Jun 14 00:22:45 2007 +0200
     1.2 +++ b/NEWS	Thu Jun 14 00:48:42 2007 +0200
     1.3 @@ -32,14 +32,9 @@
     1.4  these tend to cause confusion about the actual goal (!) context being
     1.5  used here, which is not necessarily the same as the_context().
     1.6  
     1.7 -* Command 'find_theorems': supports "*" wildcard in "name:" criterion.
     1.8 -
     1.9 -* Proof General interface: A search form for the "Find Theorems" command is
    1.10 -now available via C-c C-a C-f.  The old minibuffer interface is available
    1.11 -via C-c C-a C-m.  Variable proof-find-theorems-command (customizable via
    1.12 -'Proof-General -> Advanced -> Internals -> Prover Config') controls the
    1.13 -default behavior of 'ProofGeneral -> Find Theorems' (C-c C-f): set to
    1.14 -isar-find-theorems-form or isar-find-theorems-minibuffer.
    1.15 +* Command 'find_theorems': supports "*" wild-card in "name:"
    1.16 +criterion; "with_dups" option.  Certain ProofGeneral versions might
    1.17 +support a specific search form (see ProofGeneral/CHANGES).
    1.18  
    1.19  * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
    1.20  by default, which means that "prems" (and also "fixed variables") are