diff -r aa54cd3ddc9f -r 68e5eee47a45 NEWS
--- a/NEWS	Wed Mar 19 14:25:59 2008 +0100
+++ b/NEWS	Wed Mar 19 18:10:23 2008 +0100
@@ -132,6 +132,10 @@
 * Metis prover is now an order of magnitude faster, and also works
 with multithreading.
 
+* Sledgehammer no longer produces structured proofs by default. To enable, 
+declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus,  
+reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. 
+INCOMPATIBILITY.
 
 *** ZF ***