tuned;
authorwenzelm
Tue Feb 13 22:51:08 2001 +0100 (2001-02-13)
changeset 111122fea4923864f
parent 11111 3b8efc0ead02
child 11113 8ab6c9093508
tuned;
NEWS
     1.1 --- a/NEWS	Tue Feb 13 22:04:09 2001 +0100
     1.2 +++ b/NEWS	Tue Feb 13 22:51:08 2001 +0100
     1.3 @@ -170,9 +170,6 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* print modes "brackets" and "no_brackets" control output of nested =>
     1.8 -(types) and ==> (props); the default behaviour is "brackets";
     1.9 -
    1.10  * system: support Poly/ML 4.0;
    1.11  
    1.12  * Pure: the Simplifier has been implemented properly as a derived rule
    1.13 @@ -180,6 +177,9 @@
    1.14  penalty in practical applications is about 50%, while reliability of
    1.15  the Isabelle inference kernel has been greatly improved;
    1.16  
    1.17 +* print modes "brackets" and "no_brackets" control output of nested =>
    1.18 +(types) and ==> (props); the default behaviour is "brackets";
    1.19 +
    1.20  * Provers: fast_tac (and friends) now handle actual object-logic rules
    1.21  as assumptions as well;
    1.22