entry point for comprehensive word library
authorhaftmann
Tue Apr 16 19:50:19 2019 +0000 (7 days ago)
changeset 7017440fdd74b75f3
parent 70173 c2786fe88064
child 70175 85fb1a585f52
entry point for comprehensive word library
NEWS
src/HOL/ROOT
src/HOL/Word/More_Word.thy
     1.1 --- a/NEWS	Tue Apr 16 19:50:18 2019 +0000
     1.2 +++ b/NEWS	Tue Apr 16 19:50:19 2019 +0000
     1.3 @@ -285,6 +285,10 @@
     1.4  
     1.5  * SMT: reconstruction is now possible using the SMT solver veriT.
     1.6  
     1.7 +* Session HOL-Word:
     1.8 +  * New theory More_Word as comprehensive entrance point.
     1.9 +  INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** ML ***
    1.13  
     2.1 --- a/src/HOL/ROOT	Tue Apr 16 19:50:18 2019 +0000
     2.2 +++ b/src/HOL/ROOT	Tue Apr 16 19:50:19 2019 +0000
     2.3 @@ -829,7 +829,7 @@
     2.4      "HOL-Library"
     2.5    theories
     2.6      Word
     2.7 -    Word_Bitwise
     2.8 +    More_Word
     2.9      Word_Examples
    2.10    document_files "root.bib" "root.tex"
    2.11  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Word/More_Word.thy	Tue Apr 16 19:50:19 2019 +0000
     3.3 @@ -0,0 +1,12 @@
     3.4 +(*  Title:      HOL/Word/More_Word.thy
     3.5 +*)
     3.6 +
     3.7 +section \<open>Comprehensive Word Library\<close>
     3.8 +
     3.9 +theory More_Word
    3.10 +imports
    3.11 +  Word
    3.12 +  Word_Bitwise
    3.13 +begin
    3.14 +
    3.15 +end