--- a/NEWS Mon May 23 11:06:41 2005 +0200
+++ b/NEWS Mon May 23 11:14:58 2005 +0200
@@ -113,6 +113,9 @@
etc.) may depend on the signature of the theory context being
presently used for parsing/printing, see also isar-ref manual.
+* Pure/Simplifier: you can control the depth to which conditional rewriting
+ is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth Limit.
+
* Pure/Simplifier: simplification procedures may now take the current
simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
interface), which is very useful for calling the Simplifier