# HG changeset patch
# User wenzelm
# Date 1506955319 -7200
# Node ID 1dd5633f58629a761216e3ecf468fa106c9236a3
# Parent  1f92f5cc70e40b7d21fa0475789d2331613fb972
clarified imports: prefer parent session images;

diff -r 1f92f5cc70e4 -r 1dd5633f5862 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Oct 02 16:08:43 2017 +0200
+++ b/src/HOL/ROOT	Mon Oct 02 16:41:59 2017 +0200
@@ -409,7 +409,6 @@
   *}
   options [parallel_proofs = 0, quick_and_dirty = false]
   sessions
-    "HOL-Library"
     "HOL-Computational_Algebra"
   theories
     Greatest_Common_Divisor
@@ -524,13 +523,11 @@
   theories CompleteLattice
   document_files "root.tex"
 
-session "HOL-ex" (timing) in ex = "HOL-Library" +
+session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
   options [document = false]
-  sessions
-    "HOL-Number_Theory"
   theories
     Adhoc_Overloading_Examples
     Antiquote
@@ -719,10 +716,8 @@
     Koepf_Duermuth_Countermeasure
     Measure_Not_CCC
 
-session "HOL-Nominal" in Nominal = HOL +
+session "HOL-Nominal" in Nominal = "HOL-Library" +
   options [document = false]
-  sessions
-    "HOL-Library"
   theories
     Nominal
 
@@ -1022,15 +1017,13 @@
     "Examples/Finite"
     "Examples/T2_Spaces"
 
-session HOLCF (main timing) in HOLCF = HOL +
+session HOLCF (main timing) in HOLCF = "HOL-Library" +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
 
     HOLCF -- a semantic extension of HOL by the LCF logic.
   *}
-  sessions
-    "HOL-Library"
   theories
     HOLCF (global)
   document_files "root.tex"