--- a/CONTRIBUTORS Thu Sep 17 09:57:31 2020 +0000
+++ b/CONTRIBUTORS Thu Sep 17 12:06:38 2020 +0200
@@ -25,6 +25,10 @@
* May 2020: Florian Haftmann
Generic algebraically founded bit operations NOT, AND, OR, XOR.
+* Sept. 2020: Florian Haftmann
+ Substantial reworking and modularization of Word library, with
+ generic type conversions.
+
* June 2020: Florian Haftmann
Simproc defined_all for more aggressive substitution with variables
from assumptions.
--- a/NEWS Thu Sep 17 09:57:31 2020 +0000
+++ b/NEWS Thu Sep 17 12:06:38 2020 +0200
@@ -93,6 +93,10 @@
* Session HOL-Word: Most operations on type word are set up
for transfer and lifting. INCOMPATIBILITY.
+* Session HOL-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.