# HG changeset patch
# User wenzelm
# Date 1181774922 -7200
# Node ID d0e3f790bd73e82219004cc4d8fa5f573164ab3e
# Parent  1d138d6bb4613e5fb8974bc68773961c2373b2d7
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;

diff -r 1d138d6bb461 -r d0e3f790bd73 NEWS
--- a/NEWS	Thu Jun 14 00:22:45 2007 +0200
+++ b/NEWS	Thu Jun 14 00:48:42 2007 +0200
@@ -32,14 +32,9 @@
 these tend to cause confusion about the actual goal (!) context being
 used here, which is not necessarily the same as the_context().
 
-* Command 'find_theorems': supports "*" 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.
+* Command 'find_theorems': supports "*" wild-card in "name:"
+criterion; "with_dups" option.  Certain ProofGeneral versions might
+support a specific search form (see ProofGeneral/CHANGES).
 
 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
 by default, which means that "prems" (and also "fixed variables") are