*** empty log message ***
authornipkow
Fri, 05 Jan 2001 18:31:48 +0100
changeset 107934d6cf7702e3c
parent 10792 78dfc5904eea
child 10794 65d18005d802
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Fri Jan 05 18:16:01 2001 +0100
     1.2 +++ b/NEWS	Fri Jan 05 18:31:48 2001 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -11,6 +10,9 @@
     1.9  
    1.10  * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
    1.11  
    1.12 +* HOL: infix "dvd" now has priority 50 rather than 70
    1.13 + (because it is a relation)
    1.14 +
    1.15  * Isar: 'obtain' no longer declares "that" fact as simp/intro;
    1.16  
    1.17  * Isar/HOL: method 'induct' now handles non-atomic goals; as a