# HG changeset patch
# User paulson
# Date 1331915554 0
# Node ID 0c8fb96cce73c029a0e485f01a0d2607af9c497d
# Parent  f9533c462457ab65cb65d4372b91445465bbd65f
ZF news

diff -r f9533c462457 -r 0c8fb96cce73 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 ***