# HG changeset patch
# User wenzelm
# Date 1492858336 -7200
# Node ID e957b1f004499d859cba5da826cbf1e0b57c8a3f
# Parent  263f2a046308b94b69f04e422a5067f58e86205c
clarified parent session images, to avoid duplicate loading of theories;

diff -r 263f2a046308 -r e957b1f00449 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Apr 21 21:41:32 2017 +0200
+++ b/src/HOL/ROOT	Sat Apr 22 12:52:16 2017 +0200
@@ -62,10 +62,7 @@
     Refute
   document_files "root.bib" "root.tex"
 
-session "HOL-Analysis" (main timing) in Analysis = HOL +
-  sessions
-    "HOL-Library"
-    "HOL-Computational_Algebra"
+session "HOL-Analysis" (main timing) in Analysis = "HOL-Computational_Algebra" +
   theories
     Analysis
   document_files
@@ -76,16 +73,14 @@
     Approximations
     Circle_Area
 
-session "HOL-Computational_Algebra" in "Computational_Algebra" = HOL +
-  sessions
-    "HOL-Library"
+session "HOL-Computational_Algebra" in "Computational_Algebra" = "HOL-Library" +
   theories
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
     Field_as_Ring
     Polynomial_Factorial
 
-session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
+session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
   description {*
     Author:     Gertrud Bauer, TU Munich
 
@@ -103,13 +98,11 @@
     subspaces (not only one-dimensional subspaces), can be extended to a
     continous linearform on the whole vectorspace.
   *}
-  sessions
-    "HOL-Library"
   theories
     Hahn_Banach
   document_files "root.bib" "root.tex"
 
-session "HOL-Induct" in Induct = HOL +
+session "HOL-Induct" in Induct = "HOL-Library" +
   description {*
     Examples of (Co)Inductive Definitions.
 
@@ -126,8 +119,6 @@
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
   *}
-  sessions
-    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Old_Datatype"
   theories [quick_and_dirty]
@@ -224,15 +215,13 @@
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
-session "HOL-Number_Theory" (timing) in Number_Theory = HOL +
+session "HOL-Number_Theory" (timing) in Number_Theory = "HOL-Computational_Algebra" +
   description {*
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   *}
   sessions
-    "HOL-Library"
     "HOL-Algebra"
-    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/FuncSet"
     "~~/src/HOL/Library/Multiset"
@@ -259,11 +248,8 @@
   theories Hoare_Parallel
   document_files "root.bib" "root.tex"
 
-session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
+session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
   options [document = false, browser_info = false]
-  sessions
-    "HOL-Computational_Algebra"
-    "HOL-Number_Theory"
   theories
     Generate
     Generate_Binary_Nat
@@ -318,15 +304,12 @@
   options [document = false]
   theories Nunchaku
 
-session "HOL-Algebra" (main timing) in Algebra = HOL +
+session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
     The Isabelle Algebraic Library.
   *}
-  sessions
-    "HOL-Library"
-    "HOL-Computational_Algebra"
   theories [document = false]
     (* Preliminaries from set and number theory *)
     "~~/src/HOL/Library/FuncSet"
@@ -416,10 +399,8 @@
   theories MainZF Games
   document_files "root.tex"
 
-session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
+session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
   options [print_mode = "iff,no_brackets"]
-  sessions
-    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -427,14 +408,11 @@
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
 
-session "HOL-Decision_Procs" (timing) in Decision_Procs = HOL +
+session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   description {*
     Various decision procedures, typically involving reflection.
   *}
   options [document = false]
-  sessions
-    "HOL-Library"
-    "HOL-Algebra"
   theories
     Decision_Procs
 
@@ -500,14 +478,12 @@
   options [document = false]
   theories Test Type
 
-session "HOL-MicroJava" (timing) in MicroJava = HOL +
+session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
   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"
   theories [document = false]
     "~~/src/HOL/Library/While_Combinator"
   theories
@@ -573,13 +549,12 @@
   theories CompleteLattice
   document_files "root.tex"
 
-session "HOL-ex" in ex = HOL +
+session "HOL-ex" in ex = "HOL-Library" +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
   options [document = false]
   sessions
-    "HOL-Library"
     "HOL-Number_Theory"
   theories
     Adhoc_Overloading_Examples
@@ -666,14 +641,11 @@
   theories [skip_proofs = false]
     Meson_Test
 
-session "HOL-Isar_Examples" in Isar_Examples = HOL +
+session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
   description {*
     Miscellaneous Isabelle/Isar examples.
   *}
   options [quick_and_dirty]
-  sessions
-    "HOL-Library"
-    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Computational_Algebra/Primes"
@@ -709,12 +681,10 @@
     Examples
     Examples_FOL
 
-session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
+session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
   description {*
     Verification of the SET Protocol.
   *}
-  sessions
-    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Nat_Bijection"
   theories
@@ -766,8 +736,6 @@
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
-  sessions
-    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Permutation"
@@ -884,7 +852,7 @@
     StateSpaceEx
   document_files "root.tex"
 
-session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = HOL +
+session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
   description {*
     Nonstandard analysis.
   *}
@@ -894,8 +862,6 @@
 
 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   options [document = false]
-  sessions
-    "HOL-Computational_Algebra"
   theories
     NSPrimes
 
@@ -1029,13 +995,11 @@
     Hotel_Example
     Quickcheck_Narrowing_Examples
 
-session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL +
+session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Library" +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
   options [document = false]
-  sessions
-    "HOL-Library"
   theories
     DList
     Quotient_FSet