1.1 --- a/NEWS	Tue Aug 18 10:25:13 1998 +0200
     1.2 +++ b/NEWS	Tue Aug 18 10:27:14 1998 +0200
     1.3 @@ -227,7 +227,8 @@
     1.4  
     1.5  *** ZF ***
     1.6  
     1.7 -* theory Main includes everything;
     1.8 +* theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
     1.9 +  only the theorems proved on ZF.ML;
    1.10  
    1.11  * ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name
    1.12    was misleading).  The rule and 'sym RS equals0E' are now in the default