--- a/NEWS Thu Oct 29 09:59:40 2020 +0000
+++ b/NEWS Thu Oct 29 10:03:03 2020 +0000
@@ -109,55 +109,56 @@
* Library theory "Signed_Division" provides operations for signed
division, instantiated for type int.
-* Session HOL-Word: Type word is restricted to bit strings consisting
+* Self-contained library theory "Word" taken over from former session
+"HOL-Word".
+
+* Theory "Word": Type word is restricted to bit strings consisting
of at least one bit. INCOMPATIBILITY.
-* Session HOL-Word: Various operations dealing with bit values
-represented as reversed lists of bools are separated into theory
-Reversed_Bit_Lists, included by theory More_Word rather than theory Word.
-INCOMPATIBILITY.
-
-* Session HOL-Word: Bit operations NOT, AND, OR, XOR are based on
+* Theory "Word": Bit operations NOT, AND, OR, XOR are based on
generic algebraic bit operations from HOL-Library.Bit_Operations.
INCOMPATIBILITY.
-* Session HOL-Word: Most operations on type word are set up
+* Theory "Word": Most operations on type word are set up
for transfer and lifting. INCOMPATIBILITY.
-* Session HOL-Word: Generic type conversions. INCOMPATIBILITY,
+* Theory "Word": Generic type conversions. INCOMPATIBILITY,
sometimes additional rewrite rules must be added to applications to
get a confluent system again.
-* Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry
-Word_Lib as theory "Bitwise". INCOMPATIBILITY.
-
-* Session HOL-Word: Compound operation "bin_split" simplifies by default
-into its components "drop_bit" and "take_bit". INCOMPATIBILITY.
-
-* Session HOL-Word: Uniform polymorphic "mask" operation for both
+* Theory "Word": Uniform polymorphic "mask" operation for both
types int and word. INCOMPATIBILITY.
-* Session HOL-Word: Syntax for signed compare operators has been
+* Theory "Word": Syntax for signed compare operators has been
consolidated with syntax of regular compare operators.
Minor INCOMPATIBILITY.
-* Session HOL-Word: Operations lsb, msb and set_bit are separated
-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.
-
-* Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
-Minor INCOMPATIBILITY.
+* Former session "HOL-Word": Various operations dealing with bit values
+represented as reversed lists of bools are separated into theory
+Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.
+
+* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
+entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.
+
+* Former session "HOL-Word": Compound operation "bin_split" simplifies
+by default into its components "drop_bit" and "take_bit".
+INCOMPATIBILITY.
+
+* Former session "HOL-Word": Operations lsb, msb and set_bit are
+separated into theories Misc_lsb, Misc_msb and Misc_set_bit respectively
+in session Word_Lib in the AFP. INCOMPATIBILITY.
+
+* Former session "HOL-Word": Ancient int numeral representation has been
+factored out in separate theory "Ancient_Numeral" in session Word_Lib
+in the AFP. INCOMPATIBILITY.
+
+* Former 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.
+
+* Former session "HOL-Word": Misc ancient material has been factored out
+into separate theories and moved to session Word_Lib in the AFP. See
+theory "Guide" there for further information. INCOMPATIBILITY.
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
are in working order again, as opposed to outputting "GaveUp" on nearly