src/HOL/ROOT

--- a/src/HOL/ROOT	Tue May 12 15:52:17 2020 +0200
+++ b/src/HOL/ROOT	Tue May 12 16:29:26 2020 +0200
@@ -122,7 +122,7 @@
     "root.tex"
     "style.sty"
 
-session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
+session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
   description "
     Author:     Gertrud Bauer, TU Munich
 
@@ -146,7 +146,7 @@
     Hahn_Banach
   document_files "root.bib" "root.tex"
 
-session "HOL-Induct" in Induct = "HOL-Library" +
+session "HOL-Induct" in Induct = HOL +
   description "
     Examples of (Co)Inductive Definitions.
 
@@ -163,6 +163,8 @@
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
   "
+  sessions
+    "HOL-Library"
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -362,10 +364,11 @@
     Algebra
   document_files "root.bib" "root.tex"
 
-session "HOL-Auth" (timing) in Auth = "HOL-Library" +
+session "HOL-Auth" (timing) in Auth = HOL +
   description "
     A new approach to verifying authentication protocols.
   "
+  sessions "HOL-Library"
   directories "Smartcard" "Guard"
   theories
     Auth_Shared
@@ -420,19 +423,22 @@
     ELT
   document_files "root.tex"
 
-session "HOL-Unix" in Unix = "HOL-Library" +
+session "HOL-Unix" in Unix = HOL +
   options [print_mode = "no_brackets,no_type_brackets"]
+  sessions "HOL-Library"
   theories Unix
   document_files "root.bib" "root.tex"
 
-session "HOL-ZF" in ZF = "HOL-Library" +
+session "HOL-ZF" in ZF = HOL +
+  sessions "HOL-Library"
   theories
     MainZF
     Games
   document_files "root.tex"
 
-session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
+session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL +
   options [print_mode = "iff,no_brackets"]
+  sessions "HOL-Library"
   directories "ex"
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
@@ -500,13 +506,14 @@
   "
   theories Test Type
 
-session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
+session "HOL-MicroJava" (timing) in MicroJava = HOL +
   description "
     Formalization of a fragment of Java, together with a corresponding virtual
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
   "
   sessions
+    "HOL-Library"
     "HOL-Eisbach"
   directories "BV" "Comp" "DFA" "J" "JVM"
   theories
@@ -523,7 +530,9 @@
   theories Example
   document_files "root.bib" "root.tex"
 
-session "HOL-Bali" (timing) in Bali = "HOL-Library" +
+session "HOL-Bali" (timing) in Bali = HOL +
+  sessions
+    "HOL-Library"
   theories
     AxExample
     AxSound
@@ -712,18 +721,21 @@
     Examples_FOL
     Example_Metric
 
-session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
+session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
   description "
     Verification of the SET Protocol.
   "
+  sessions
+    "HOL-Library"
   theories
     SET_Protocol
   document_files "root.tex"
 
-session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
+session "HOL-Matrix_LP" in Matrix_LP = HOL +
   description "
     Two-dimensional matrices and linear programming.
   "
+  sessions "HOL-Library"
   directories "Compute_Oracle"
   theories Cplex
   document_files "root.tex"
@@ -743,7 +755,7 @@
 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   theories MemoryImplementation
 
-session "HOL-TPTP" in TPTP = "HOL-Library" +
+session "HOL-TPTP" in TPTP = HOL +
   description "
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Nik Sultana, University of Cambridge
@@ -751,6 +763,8 @@
 
     TPTP-related extensions.
   "
+  sessions
+    "HOL-Library"
   theories
     ATP_Theory_Export
     MaSh_Eval
@@ -771,7 +785,8 @@
     Koepf_Duermuth_Countermeasure
     Measure_Not_CCC
 
-session "HOL-Nominal" in Nominal = "HOL-Library" +
+session "HOL-Nominal" in Nominal = HOL +
+  sessions "HOL-Library"
   theories
     Nominal
 
@@ -944,10 +959,12 @@
     "Simple_Gcd.adb"
     "Simple_Gcd.ads"
 
-session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
+session "HOL-Mutabelle" in Mutabelle = HOL +
+  sessions "HOL-Library"
   theories MutabelleExtra
 
-session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
+session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
+  sessions "HOL-Library"
   theories
     Quickcheck_Examples
     Quickcheck_Lattice_Examples
@@ -975,7 +992,8 @@
     Int_Pow
     Lifting_Code_Dt_Test
 
-session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
+session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
+  sessions "HOL-Library"
   theories
     Examples
     Predicate_Compile_Tests