isabelle-2021: HOL-Word now in HOL-Library

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

docs/setup.md

@@ -110,7 +110,7 @@ mkdir -p ~/.isabelle/etc
 cp -i misc/etc/settings ~/.isabelle/etc/settings
 ./isabelle/bin/isabelle components -a
 ./isabelle/bin/isabelle jedit -bf
-./isabelle/bin/isabelle build -bv HOL-Word
+./isabelle/bin/isabelle build -bv HOL
 ```
 
 These commands perform the following steps:
@@ -121,13 +121,13 @@ These commands perform the following steps:
   Isabelle `contrib` tools from the Munich Isabelle repository and set up
   paths such that multiple Isabelle repository installations can be used
   side by side without interfering with each other.
-* download `contrib` components from either the Munich or TS repository. This includes
+* download `contrib` components from the Isabelle repository. This includes
   Scala, a Java JDK, PolyML, and multiple external provers. You should
   download these, even if you have these tools previously installed
   elsewhere to make sure you have the right versions. Depending on your
   internet connection, this may take some time.
 * compile and build the Isabelle PIDE jEdit interface.
-* build basic Isabelle images, including `HOL-Word` to ensure that
+* build basic Isabelle images to ensure that
   the installation works. This may take a few minutes.
 
 Alternatively, it is possible to use the official Isabelle2020 release

lib/Lib.thy

@@ -20,7 +20,7 @@ imports
   Eval_Bool
   NICTATools
   "HOL-Library.Prefix_Order"
-  "HOL-Word.Word"
+  "HOL-Library.Word" (* FIXME: this should not be necessary *)
 begin
 
 (* FIXME: eliminate *)

lib/NatBitwise.thy

@@ -8,7 +8,6 @@
  * Lemmas about this instance should also go here. *)
 theory NatBitwise
 imports
-  "HOL-Word.Word"
   Lib
 begin
 

lib/sep_algebra/ex/capDL/Types_D.thy

@@ -12,7 +12,7 @@
 chapter "A simplified version of the actual capDL specification."
 
 theory Types_D
-imports "HOL-Word.Word"
+imports "HOL-Library.Word"
 begin
 
 (*

misc/regression/tests.xml

@@ -51,7 +51,7 @@
   -->
 <testsuite>
 
-  <!-- Build Isabelle and common theories (Pure, HOL, HOL-Word, Word). -->
+  <!-- Build Isabelle and common theories (Pure, HOL, Word). -->
   <sequence>
     <test name="isabelle" cwd="../.." cpu-timeout="3600">isabelle/bin/isabelle build -d . -vb Word_Lib</test>
   </sequence>

misc/scripts/thydeps

@@ -50,7 +50,7 @@ def session_theory_deps(isabelle_dir, ROOT_dirs, sessions):
     for l in run_isabelle_tool(
             isabelle_dir, cmdline, ignore_exit_code=True).splitlines():
         l = l.decode('utf-8')
-        # 'Session HOL/HOL-Word (main timing)'
+        # 'Session HOL/HOL-Library (main timing)'
         m = re.match(r'Session (' + session_name_re + ')/(' + session_name_re + ')(?: \(.*\))?', l)
         if m:
             # start processing next session

tools/c-parser/ROOT

@@ -15,7 +15,6 @@ session "Simpl-VCG" in Simpl = Word_Lib +
 session CParser = "Simpl-VCG" +
   sessions
     "HOL-Library"
-    "HOL-Word"
     "Lib"
   directories
     "umm_heap"

tools/c-parser/umm_heap/ARM/Addr_Type.thy

@@ -7,7 +7,7 @@
 (* License: BSD, terms see file ./LICENSE *)
 
 theory Addr_Type
-imports "HOL-Word.Word"
+imports "HOL-Library.Word"
 begin
 
 type_synonym addr_bitsize = "32"

tools/c-parser/umm_heap/ARM_HYP/Addr_Type.thy

@@ -7,7 +7,7 @@
 (* License: BSD, terms see file ./LICENSE *)
 
 theory Addr_Type
-imports "HOL-Word.Word"
+imports "HOL-Library.Word"
 begin
 
 type_synonym addr_bitsize = "32"

tools/c-parser/umm_heap/RISCV64/Addr_Type.thy

@@ -7,7 +7,7 @@
 (* License: BSD, terms see file ./LICENSE *)
 
 theory Addr_Type
-imports "HOL-Word.Word"
+imports "HOL-Library.Word"
 begin
 
 type_synonym addr_bitsize = "64"

tools/c-parser/umm_heap/X64/Addr_Type.thy

@@ -7,7 +7,7 @@
 (* License: BSD, terms see file ./LICENSE *)
 
 theory Addr_Type
-imports "HOL-Word.Word"
+imports "HOL-Library.Word"
 begin
 
 type_synonym addr_bitsize = "64"