changeset 55818 | d8b2f50705d0 |
parent 55757 | 9fc71814b8c1 |
child 55867 | 79b915f26533 |
--- 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.