NEWS

--- a/NEWS	Wed Sep 30 08:22:07 2009 +0200
+++ b/NEWS	Wed Sep 30 08:28:23 2009 +0200
@@ -18,6 +18,10 @@
 
 *** HOL ***
 
+* Most rules produced by inductive and datatype package
+have mandatory prefixes.
+INCOMPATIBILITY.
+
 * New proof method "smt" for a combination of first-order logic
 with equality, linear and nonlinear (natural/integer/real)
 arithmetic, and fixed-size bitvectors; there is also basic