clarified imports: prefer parent session images;
authorwenzelm
Mon Oct 02 16:41:59 2017 +0200 (19 months ago)
changeset 667521dd5633f5862
parent 66751 1f92f5cc70e4
child 66753 f7759beab4f2
clarified imports: prefer parent session images;
src/HOL/ROOT
     1.1 --- a/src/HOL/ROOT	Mon Oct 02 16:08:43 2017 +0200
     1.2 +++ b/src/HOL/ROOT	Mon Oct 02 16:41:59 2017 +0200
     1.3 @@ -409,7 +409,6 @@
     1.4    *}
     1.5    options [parallel_proofs = 0, quick_and_dirty = false]
     1.6    sessions
     1.7 -    "HOL-Library"
     1.8      "HOL-Computational_Algebra"
     1.9    theories
    1.10      Greatest_Common_Divisor
    1.11 @@ -524,13 +523,11 @@
    1.12    theories CompleteLattice
    1.13    document_files "root.tex"
    1.14  
    1.15 -session "HOL-ex" (timing) in ex = "HOL-Library" +
    1.16 +session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
    1.17    description {*
    1.18      Miscellaneous examples for Higher-Order Logic.
    1.19    *}
    1.20    options [document = false]
    1.21 -  sessions
    1.22 -    "HOL-Number_Theory"
    1.23    theories
    1.24      Adhoc_Overloading_Examples
    1.25      Antiquote
    1.26 @@ -719,10 +716,8 @@
    1.27      Koepf_Duermuth_Countermeasure
    1.28      Measure_Not_CCC
    1.29  
    1.30 -session "HOL-Nominal" in Nominal = HOL +
    1.31 +session "HOL-Nominal" in Nominal = "HOL-Library" +
    1.32    options [document = false]
    1.33 -  sessions
    1.34 -    "HOL-Library"
    1.35    theories
    1.36      Nominal
    1.37  
    1.38 @@ -1022,15 +1017,13 @@
    1.39      "Examples/Finite"
    1.40      "Examples/T2_Spaces"
    1.41  
    1.42 -session HOLCF (main timing) in HOLCF = HOL +
    1.43 +session HOLCF (main timing) in HOLCF = "HOL-Library" +
    1.44    description {*
    1.45      Author:     Franz Regensburger
    1.46      Author:     Brian Huffman
    1.47  
    1.48      HOLCF -- a semantic extension of HOL by the LCF logic.
    1.49    *}
    1.50 -  sessions
    1.51 -    "HOL-Library"
    1.52    theories
    1.53      HOLCF (global)
    1.54    document_files "root.tex"