# HG changeset patch
# User paulson
# Date 903428834 -7200
# Node ID cd53e59688a82ba1a4e67ce022975964eaffc71b
# Parent  3d27b96a08b02ad0c7d5a97cb09769f7e6b3019d
ZF.thy

diff -r 3d27b96a08b0 -r cd53e59688a8 NEWS
--- a/NEWS	Tue Aug 18 10:25:13 1998 +0200
+++ b/NEWS	Tue Aug 18 10:27:14 1998 +0200
@@ -227,7 +227,8 @@
 
 *** ZF ***
 
-* theory Main includes everything;
+* theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
+  only the theorems proved on ZF.ML;
 
 * ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name
   was misleading).  The rule and 'sym RS equals0E' are now in the default