src/HOL/ROOT
changeset 50844 b95ff3744815
parent 50833 133a38b7ceaf
child 50870 b8606dd29783
     1.1 --- a/src/HOL/ROOT	Sat Jan 12 14:53:56 2013 +0100
     1.2 +++ b/src/HOL/ROOT	Sat Jan 12 14:56:57 2013 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4      "Tools/Quickcheck/Narrowing_Engine.hs"
     1.5      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     1.6  
     1.7 -session "HOL-Library" in Library = HOL +
     1.8 +session "HOL-Library" (main) in Library = HOL +
     1.9    description {* Classical Higher-order Logic -- batteries included *}
    1.10    theories
    1.11      Library
    1.12 @@ -178,7 +178,7 @@
    1.13    options [document = false]
    1.14    theories [quick_and_dirty] Nitpick_Examples
    1.15  
    1.16 -session "HOL-Algebra" in Algebra = HOL +
    1.17 +session "HOL-Algebra" (main) in Algebra = HOL +
    1.18    description {*
    1.19      Author: Clemens Ballarin, started 24 September 1999
    1.20  
    1.21 @@ -553,7 +553,7 @@
    1.22    theories [proofs = 0]  (* FIXME !? *)
    1.23      ATP_Problem_Import
    1.24  
    1.25 -session "HOL-Multivariate_Analysis" in Multivariate_Analysis = HOL +
    1.26 +session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
    1.27    options [document_graph]
    1.28    theories
    1.29      Multivariate_Analysis
    1.30 @@ -620,7 +620,7 @@
    1.31      Misc_Codata
    1.32      Misc_Data
    1.33  
    1.34 -session "HOL-Word" in Word = HOL +
    1.35 +session "HOL-Word" (main) in Word = HOL +
    1.36    options [document_graph]
    1.37    theories Word
    1.38    files "document/root.bib" "document/root.tex"
    1.39 @@ -680,7 +680,7 @@
    1.40      "VCC_Max.b2i"
    1.41      "VCC_Max.certs"
    1.42  
    1.43 -session "HOL-SPARK" in "SPARK" = "HOL-Word" +
    1.44 +session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
    1.45    options [document = false]
    1.46    theories SPARK
    1.47