# HG changeset patch
# User webertj
# Date 1179141862 -7200
# Node ID b81bbe2984066e3ddddab6763886b5a71cd7e8c6
# Parent  2284e0d02e7f951062a48a36b2fa4472b565eb2d
ProofGeneral: Find Theorems search form

diff -r 2284e0d02e7f -r b81bbe298406 NEWS
--- a/NEWS	Mon May 14 12:52:56 2007 +0200
+++ b/NEWS	Mon May 14 13:24:22 2007 +0200
@@ -33,6 +33,13 @@
 
 * Command 'find_theorems': support "*" wildcard in "name:" criterion.
 
+* Proof General interface: A search form for the "Find Theorems" command is
+now available via C-c C-a C-f.  The old minibuffer interface is available
+via C-c C-a C-m.  Variable proof-find-theorems-command (customizable via
+'Proof-General -> Advanced -> Internals -> Prover Config') controls the
+default behavior of 'ProofGeneral -> Find Theorems' (C-c C-f): set to
+isar-find-theorems-form or isar-find-theorems-minibuffer.
+
 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
 by default, which means that "prems" (and also "fixed variables") are
 suppressed from proof state output.  Note that the ProofGeneral