# HG changeset patch
# User nipkow
# Date 1046196495 -3600
# Node ID af0218406395b442789f636fbf31ec08885304f8
# Parent  fb6ec40dd291510d3ef057618cbbec26f7217bff
*** empty log message ***

diff -r fb6ec40dd291 -r af0218406395 NEWS
--- a/NEWS	Tue Feb 25 18:49:23 2003 +0100
+++ b/NEWS	Tue Feb 25 19:08:15 2003 +0100
@@ -37,6 +37,14 @@
 
   - The simplifier trace now shows the names of the applied rewrite rules
 
+  - You can limit the number of recursive invocations of the simplifier
+    during conditional rewriting (where the simplifie tries to solve the
+    conditions before applying the rewrite rule):
+    ML "simp_depth_limit := n"
+    where n is an integer. Thus you can force termination where previously
+    the simplifier would diverge.
+
+
 * Pure: New flag for triggering if the overall goal of a proof state should
 be printed:
    PG menu: Isabelle/Isar -> Settigs -> Show Main Goal