author | paulson |
Tue, 18 Aug 1998 10:27:14 +0200 | |
changeset 5332 | cd53e59688a8 |
parent 5331 | 3d27b96a08b0 |
child 5333 | ea33e66dcedd |
--- 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