--- 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