clarified parent session images, to avoid duplicate loading of theories;
authorwenzelm
Sun Apr 23 23:49:14 2017 +0200 (2017-04-23)
changeset 655693cb6f3281ef1
parent 65568 1070be576372
child 65570 660df4a6dc59
clarified parent session images, to avoid duplicate loading of theories;
src/Doc/ROOT
src/HOL/ROOT
src/ZF/ROOT
     1.1 --- a/src/Doc/ROOT	Sun Apr 23 23:10:33 2017 +0200
     1.2 +++ b/src/Doc/ROOT	Sun Apr 23 23:49:14 2017 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4      "root.tex"
     1.5      "style.sty"
     1.6  
     1.7 -session Codegen_Basics in "Codegen" = "HOL" +
     1.8 +session Codegen_Basics in "Codegen" = "HOL-Library" +
     1.9    options [document = false]
    1.10    theories
    1.11      Setup
    1.12 @@ -44,7 +44,7 @@
    1.13      "root.tex"
    1.14      "style.sty"
    1.15  
    1.16 -session Corec (doc) in "Corec" = HOL +
    1.17 +session Corec (doc) in "Corec" = "HOL-Library" +
    1.18    options [document_variants = "corec"]
    1.19    theories [document = false] "../Datatypes/Setup"
    1.20    theories Corec
    1.21 @@ -60,7 +60,7 @@
    1.22      "root.tex"
    1.23      "style.sty"
    1.24  
    1.25 -session Datatypes (doc) in "Datatypes" = HOL +
    1.26 +session Datatypes (doc) in "Datatypes" = "HOL-Library" +
    1.27    options [document_variants = "datatypes"]
    1.28    theories [document = false] Setup
    1.29    theories Datatypes
     2.1 --- a/src/HOL/ROOT	Sun Apr 23 23:10:33 2017 +0200
     2.2 +++ b/src/HOL/ROOT	Sun Apr 23 23:49:14 2017 +0200
     2.3 @@ -690,7 +690,7 @@
     2.4      SET_Protocol
     2.5    document_files "root.tex"
     2.6  
     2.7 -session "HOL-Matrix_LP" in Matrix_LP = HOL +
     2.8 +session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
     2.9    description {*
    2.10      Two-dimensional matrices and linear programming.
    2.11    *}
    2.12 @@ -982,7 +982,7 @@
    2.13    options [document = false]
    2.14    theories MutabelleExtra
    2.15  
    2.16 -session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
    2.17 +session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
    2.18    options [document = false]
    2.19    theories
    2.20      Quickcheck_Examples
    2.21 @@ -994,7 +994,7 @@
    2.22      Hotel_Example
    2.23      Quickcheck_Narrowing_Examples
    2.24  
    2.25 -session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Library" +
    2.26 +session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
    2.27    description {*
    2.28      Author:     Cezary Kaliszyk and Christian Urban
    2.29    *}
    2.30 @@ -1012,7 +1012,7 @@
    2.31      Int_Pow
    2.32      Lifting_Code_Dt_Test
    2.33  
    2.34 -session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
    2.35 +session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
    2.36    options [document = false]
    2.37    theories
    2.38      Examples
     3.1 --- a/src/ZF/ROOT	Sun Apr 23 23:10:33 2017 +0200
     3.2 +++ b/src/ZF/ROOT	Sun Apr 23 23:49:14 2017 +0200
     3.3 @@ -198,7 +198,7 @@
     3.4    options [document = false]
     3.5    theories Confluence
     3.6  
     3.7 -session "ZF-UNITY" (timing ZF) in UNITY = ZF +
     3.8 +session "ZF-UNITY" (timing ZF) in UNITY = "ZF-Induct" +
     3.9    description {*
    3.10      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.11      Copyright   1998  University of Cambridge