entry point for comprehensive word library
authorhaftmann
Tue, 16 Apr 2019 19:50:19 +0000
changeset 70174 40fdd74b75f3
parent 70173 c2786fe88064
child 70175 85fb1a585f52
entry point for comprehensive word library
NEWS
src/HOL/ROOT
src/HOL/Word/More_Word.thy
--- 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