NEWS

--- a/NEWS	Fri Mar 16 16:29:51 2012 +0000
+++ b/NEWS	Fri Mar 16 16:32:34 2012 +0000
@@ -1723,6 +1723,13 @@
 * All constant names are now qualified internally and use proper
 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
 
+*** ZF ***
+
+* Greater support for structured proofs involving induction or case analysis.
+
+* Much greater use of special symbols.
+
+* Removal of many ML theorem bindings. INCOMPATIBILITY.
 
 *** ML ***