diff -r 0bc0217387a5 -r d8b2f50705d0 NEWS --- a/NEWS Sat Mar 01 09:34:08 2014 +0100 +++ b/NEWS Sat Mar 01 17:08:39 2014 +0100 @@ -91,6 +91,13 @@ *** HOL *** +* HOL-Word: + * Abandoned fact collection "word_arith_alts", which is a + duplicate of "word_arith_wis". + * Dropped first (duplicated) element in fact collections + "sint_word_ariths", "word_arith_alts", "uint_word_ariths", + "uint_word_arith_bintrs". + * Code generator: explicit proof contexts in many ML interfaces. INCOMPATIBILITY.