NEWS
changeset 13938 b033b53d0c1e
parent 13899 12c7029d278b
child 13953 65b76920e108
     1.1 --- a/NEWS	Wed Apr 30 17:53:47 2003 +0200
     1.2 +++ b/NEWS	Wed Apr 30 18:30:57 2003 +0200
     1.3 @@ -46,6 +46,9 @@
     1.4  
     1.5    - Accepts free variables as head terms in congruence rules.  Useful in Isar.
     1.6  
     1.7 +  - No longer aborts on failed congruence proof.  Instead, the
     1.8 +    congruence is ignored.
     1.9 +
    1.10  * Pure: The main goal of the proof state is no longer shown by default, only
    1.11  the subgoals. This behaviour is controlled by a new flag.
    1.12     PG menu: Isabelle/Isar -> Settings -> Show Main Goal