NEWS
changeset 13829 af0218406395
parent 13824 e4d8dea6dfc2
child 13835 12b2ffbe543a
     1.1 --- a/NEWS	Tue Feb 25 18:49:23 2003 +0100
     1.2 +++ b/NEWS	Tue Feb 25 19:08:15 2003 +0100
     1.3 @@ -37,6 +37,14 @@
     1.4  
     1.5    - The simplifier trace now shows the names of the applied rewrite rules
     1.6  
     1.7 +  - You can limit the number of recursive invocations of the simplifier
     1.8 +    during conditional rewriting (where the simplifie tries to solve the
     1.9 +    conditions before applying the rewrite rule):
    1.10 +    ML "simp_depth_limit := n"
    1.11 +    where n is an integer. Thus you can force termination where previously
    1.12 +    the simplifier would diverge.
    1.13 +
    1.14 +
    1.15  * Pure: New flag for triggering if the overall goal of a proof state should
    1.16  be printed:
    1.17     PG menu: Isabelle/Isar -> Settigs -> Show Main Goal