# HG changeset patch
# User wenzelm
# Date 1116773462 -7200
# Node ID 3010430d894d077e5be83728087aa6b867c4d404
# Parent  4ae42d8f2fea4907d20600fcc49178d31f98d898
removed find_rewrites (superceded by improved thms_containing);

diff -r 4ae42d8f2fea -r 3010430d894d NEWS
--- a/NEWS	Fri May 20 18:35:10 2005 +0200
+++ b/NEWS	Sun May 22 16:51:02 2005 +0200
@@ -22,13 +22,13 @@
 * Theory loader: parent theories can now also be referred to via
   relative and absolute paths.
 
-* Provers/quasi.ML:  new transitivity reasoners for transitivity only
+* Provers/quasi.ML: new transitivity reasoners for transitivity only
   and quasi orders.
 
-* Provers/trancl.ML:  new transitivity reasoner for transitive and
+* Provers/trancl.ML: new transitivity reasoner for transitive and
   reflexive-transitive closure of relations.
 
-* Provers/blast.ML:  new reference depth_limit to make blast's depth
+* Provers/blast.ML: new reference depth_limit to make blast's depth
   limit (previously hard-coded with a value of 20) user-definable.
 
 * Provers: new version of the subst method, for single-step rewriting: it now
@@ -121,13 +121,8 @@
   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 declared as 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.
-
-* Isar debugging: new reference Toplevel.debug; default false.
-  Set to make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
+* Isar debugging: new reference Toplevel.debug; default false.  Set to
+  make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
   
 * Locales:
   - "includes" disallowed in declaration of named locales (command "locale").
@@ -176,6 +171,10 @@
   CPure.elim / CPure.dest attributes) now appear in the Pure name
   space; use isatool fixcpure to adapt your theory and ML sources.
 
+* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup
+  is peformed already.  Object-logics merely need to finish their
+  initial simpset configuration as before.
+
 
 *** Document preparation ***