# HG changeset patch
# User nipkow
# Date 1102956292 -3600
# Node ID 75a2ca90693e78c772dae481ce2b407930e0ccde
# Parent  010ea63b7a677345a51635863e82364aac999114
*** empty log message ***

diff -r 010ea63b7a67 -r 75a2ca90693e NEWS
--- a/NEWS	Mon Dec 13 17:07:47 2004 +0100
+++ b/NEWS	Mon Dec 13 17:44:52 2004 +0100
@@ -92,6 +92,11 @@
   Moreover, the low-level mk_simproc no longer applies Logic.varify
   internally, to allow for use in a context of fixed variables.
 
+* Pure/Simplifier: Command "find_rewrites" takes a string and lists all
+  equality theorems (not just those with attribute simp!) whose left-hand
+  side matches the term given via the string. In PG the command can be
+  activated via Isabelle -> Show me -> matching rewrites.
+
 * Provers: Simplifier and Classical Reasoner now support proof context
   dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
   components are stored in the theory and patched into the