diff -r ccc104786829 -r 4a58c38b85ff NEWS --- a/NEWS Thu Sep 24 20:29:07 2020 +0200 +++ b/NEWS Fri Sep 25 05:26:09 2020 +0000 @@ -103,13 +103,6 @@ * Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry Word_Lib as theory "Bitwise". INCOMPATIBILITY. -* Session HOL-Word: Misc ancient material has been factored out into -separate theories. INCOMPATIBILITY, prefer theory "More_Word" -over "Word" to use it. - -* Session HOL-Word: Ancient int numeral representation has been -factored out in separate theory "Ancient_Numeral". INCOMPATIBILITY. - * Session HOL-Word: Compound operation "bin_split" simplifies by default into its components "drop_bit" and "take_bit". INCOMPATIBILITY. @@ -120,6 +113,13 @@ into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. INCOMPATIBILITY. +* Session HOL-Word: Misc ancient material has been factored out into +separate theories. INCOMPATIBILITY, prefer theory "More_Word" +over "Word" to use it. + +* Session HOL-Word: Ancient int numeral representation has been +factored out in separate theory "Ancient_Numeral". INCOMPATIBILITY. + * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.