# HG changeset patch
# User haftmann
# Date 1555444219 0
# Node ID 40fdd74b75f3153faa942f3a3b8e7518cc1240ed
# Parent  c2786fe88064c202f6b0ee6557f63e3eff9741aa
entry point for comprehensive word library

diff -r c2786fe88064 -r 40fdd74b75f3 NEWS
--- 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 ***
 
diff -r c2786fe88064 -r 40fdd74b75f3 src/HOL/ROOT
--- 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"
 
diff -r c2786fe88064 -r 40fdd74b75f3 src/HOL/Word/More_Word.thy
--- /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