ZF/Main

--- a/NEWS	Thu Dec 20 15:23:42 2001 +0100
+++ b/NEWS	Thu Dec 20 15:57:29 2001 +0100
@@ -251,6 +251,9 @@
 
 *** ZF ***
 
+* Theory Main no longer includes AC; for the Axiom of Choice, base your 
+theory on Main_ZFC;
+
 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
 typeless version of the formalism;