diff -r 72fbe711e414 -r 35be762f58f9 NEWS
--- a/NEWS	Tue Jun 29 11:18:34 2004 +0200
+++ b/NEWS	Wed Jun 30 00:42:59 2004 +0200
@@ -6,6 +6,11 @@
 
 *** General ***
 
+* Pure: Simplification procedures can now take the current simpset as
+  an additional argument; This is useful for calling the simplifier
+  recursively.  See the functions MetaSimplifier.full_{mk_simproc,
+  simproc,simproc_i}.
+
 * Pure: considerably improved version of 'constdefs' command.  Now
   performs automatic type-inference of declared constants; additional
   support for local structure declarations (cf. locales and HOL