src/HOL/ROOT

   theories Main
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
-session "HOL-Library" in Library = HOL +
+session "HOL-Library" (main) in Library = HOL +
   description {* Classical Higher-order Logic -- batteries included *}
   theories
     Library
     Sublist
     List_lexord

     Copyright   2009
   *}
   options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
-session "HOL-Algebra" in Algebra = HOL +
+session "HOL-Algebra" (main) in Algebra = HOL +
   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
     The Isabelle Algebraic Library.
   *}

     TPTP_Interpret
     THF_Arith
   theories [proofs = 0]  (* FIXME !? *)
     ATP_Problem_Import
 
-session "HOL-Multivariate_Analysis" in Multivariate_Analysis = HOL +
+session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   options [document_graph]
   theories
     Multivariate_Analysis
     Determinants
   files

     Koenig
   theories [condition = ISABELLE_FULL_TEST]
     Misc_Codata
     Misc_Data
 
-session "HOL-Word" in Word = HOL +
+session "HOL-Word" (main) in Word = HOL +
   options [document_graph]
   theories Word
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +

     "Boogie_Max.b2i"
     "Boogie_Max.certs"
     "VCC_Max.b2i"
     "VCC_Max.certs"
 
-session "HOL-SPARK" in "SPARK" = "HOL-Word" +
+session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   options [document = false]
   theories SPARK
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   options [document = false]