--- a/NEWS Fri Mar 26 20:30:03 2010 +0100
+++ b/NEWS Fri Mar 26 23:46:22 2010 +0100
@@ -61,6 +61,15 @@
* Use of cumulative prems via "!" in some proof methods has been
discontinued (legacy feature).
+* References 'trace_simp' and 'debug_simp' have been replaced by
+configuration options stored in the context. Enabling tracing
+(the case of debugging is similar) in proofs works via
+
+ using [[trace_simp=true]]
+
+Tracing is then active for all invocations of the simplifier
+in subsequent goal refinement steps.
+
*** Pure ***