ProofGeneral: Find Theorems search form
authorwebertj
Mon May 14 13:24:22 2007 +0200 (2007-05-14)
changeset 22965b81bbe298406
parent 22964 2284e0d02e7f
child 22966 9dc4f5048353
ProofGeneral: Find Theorems search form
NEWS
     1.1 --- a/NEWS	Mon May 14 12:52:56 2007 +0200
     1.2 +++ b/NEWS	Mon May 14 13:24:22 2007 +0200
     1.3 @@ -33,6 +33,13 @@
     1.4  
     1.5  * Command 'find_theorems': support "*" wildcard in "name:" criterion.
     1.6  
     1.7 +* Proof General interface: A search form for the "Find Theorems" command is
     1.8 +now available via C-c C-a C-f.  The old minibuffer interface is available
     1.9 +via C-c C-a C-m.  Variable proof-find-theorems-command (customizable via
    1.10 +'Proof-General -> Advanced -> Internals -> Prover Config') controls the
    1.11 +default behavior of 'ProofGeneral -> Find Theorems' (C-c C-f): set to
    1.12 +isar-find-theorems-form or isar-find-theorems-minibuffer.
    1.13 +
    1.14  * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
    1.15  by default, which means that "prems" (and also "fixed variables") are
    1.16  suppressed from proof state output.  Note that the ProofGeneral