--- a/NEWS Tue Apr 16 19:50:18 2019 +0000
+++ b/NEWS Tue Apr 16 19:50:19 2019 +0000
@@ -285,6 +285,10 @@
* SMT: reconstruction is now possible using the SMT solver veriT.
+* Session HOL-Word:
+ * New theory More_Word as comprehensive entrance point.
+ INCOMPATIBILITY.
+
*** ML ***
--- a/src/HOL/ROOT Tue Apr 16 19:50:18 2019 +0000
+++ b/src/HOL/ROOT Tue Apr 16 19:50:19 2019 +0000
@@ -829,7 +829,7 @@
"HOL-Library"
theories
Word
- Word_Bitwise
+ More_Word
Word_Examples
document_files "root.bib" "root.tex"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/More_Word.thy Tue Apr 16 19:50:19 2019 +0000
@@ -0,0 +1,12 @@
+(* Title: HOL/Word/More_Word.thy
+*)
+
+section \<open>Comprehensive Word Library\<close>
+
+theory More_Word
+imports
+ Word
+ Word_Bitwise
+begin
+
+end