# HG changeset patch
# User wenzelm
# Date 1492984154 -7200
# Node ID 3cb6f3281ef1927713a90308a346ec81b5e37095
# Parent  1070be5763725cefae548ab593a9c7418de6ec6d
clarified parent session images, to avoid duplicate loading of theories;

diff -r 1070be576372 -r 3cb6f3281ef1 src/Doc/ROOT
--- a/src/Doc/ROOT	Sun Apr 23 23:10:33 2017 +0200
+++ b/src/Doc/ROOT	Sun Apr 23 23:49:14 2017 +0200
@@ -16,7 +16,7 @@
     "root.tex"
     "style.sty"
 
-session Codegen_Basics in "Codegen" = "HOL" +
+session Codegen_Basics in "Codegen" = "HOL-Library" +
   options [document = false]
   theories
     Setup
@@ -44,7 +44,7 @@
     "root.tex"
     "style.sty"
 
-session Corec (doc) in "Corec" = HOL +
+session Corec (doc) in "Corec" = "HOL-Library" +
   options [document_variants = "corec"]
   theories [document = false] "../Datatypes/Setup"
   theories Corec
@@ -60,7 +60,7 @@
     "root.tex"
     "style.sty"
 
-session Datatypes (doc) in "Datatypes" = HOL +
+session Datatypes (doc) in "Datatypes" = "HOL-Library" +
   options [document_variants = "datatypes"]
   theories [document = false] Setup
   theories Datatypes
diff -r 1070be576372 -r 3cb6f3281ef1 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Apr 23 23:10:33 2017 +0200
+++ b/src/HOL/ROOT	Sun Apr 23 23:49:14 2017 +0200
@@ -690,7 +690,7 @@
     SET_Protocol
   document_files "root.tex"
 
-session "HOL-Matrix_LP" in Matrix_LP = HOL +
+session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
   description {*
     Two-dimensional matrices and linear programming.
   *}
@@ -982,7 +982,7 @@
   options [document = false]
   theories MutabelleExtra
 
-session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
+session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   options [document = false]
   theories
     Quickcheck_Examples
@@ -994,7 +994,7 @@
     Hotel_Example
     Quickcheck_Narrowing_Examples
 
-session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Library" +
+session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
@@ -1012,7 +1012,7 @@
     Int_Pow
     Lifting_Code_Dt_Test
 
-session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
+session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   options [document = false]
   theories
     Examples
diff -r 1070be576372 -r 3cb6f3281ef1 src/ZF/ROOT
--- a/src/ZF/ROOT	Sun Apr 23 23:10:33 2017 +0200
+++ b/src/ZF/ROOT	Sun Apr 23 23:49:14 2017 +0200
@@ -198,7 +198,7 @@
   options [document = false]
   theories Confluence
 
-session "ZF-UNITY" (timing ZF) in UNITY = ZF +
+session "ZF-UNITY" (timing ZF) in UNITY = "ZF-Induct" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge