diff -r da42b500a6aa -r 8170e5327c02 NEWS
--- a/NEWS	Sat Jun 01 14:26:04 2013 +0200
+++ b/NEWS	Sun Jun 02 07:46:40 2013 +0200
@@ -61,6 +61,12 @@
 
 *** HOL ***
 
+* Reification and reflection:
+  * Reification is now directly available in HOL-Main in structure "Reification".
+  * Reflection now handles multiple lists with variables also.
+  * The whole reflection stack has been decomposed into conversions.
+INCOMPATIBILITY.
+
 * Weaker precendence of syntax for big intersection and union on sets,
 in accordance with corresponding lattice operations.  INCOMPATIBILITY.