diff -r 82dd239e0f65 -r 8b1c0d434824 NEWS
--- a/NEWS	Tue Jan 15 16:19:21 2008 +0100
+++ b/NEWS	Tue Jan 15 16:19:23 2008 +0100
@@ -25,8 +25,14 @@
 
 *** HOL ***
 
+* Merged theories IntDef, Numeral and IntArith into unified theory Int.
+INCOMPATIBILITY.
+
+* Theory Library/Code_Index: type "index" now represents natural numbers rather
+than integers.  INCOMPATIBILITY.
+
 * New class "uminus" with operation "uminus" (split of from class "minus"
-which now only has operation "minus", binary).
+which now only has operation "minus", binary).  INCOMPATIBILITY.
 
 * New primrec package.  Specification syntax conforms in style to
 definition/function/....  No separate induction rule is provided.
@@ -40,14 +46,14 @@
 * Library/ListSpace: new theory of arithmetic vector operations.
 
 * Constants "card", "internal_split", "option_map" now with authentic
-syntax.
+syntax.  INCOMPATIBILITY.
 
 * Definitions subset_def, psubset_def, set_diff_def, Compl_def,
 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,
 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,
 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,
 Sup_set_def, le_def, less_def, option_map_def now with object
-equality.
+equality.  INCOMPATIBILITY.
 
 * New method "induction_scheme" derives user-specified induction rules
 from wellfounded induction and completeness of patterns. This factors