NEWS
changeset 72292 4a58c38b85ff
parent 72281 beeadb35e357
child 72299 0c7a74a1c6d9
--- 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.