src/HOL/ROOT
changeset 48509 4854ced3e9d7
parent 48508 5a59e4c03957
child 48512 a69d7dc49f41
--- a/src/HOL/ROOT	Thu Jul 26 11:52:08 2012 +0200
+++ b/src/HOL/ROOT	Thu Jul 26 12:27:47 2012 +0200
@@ -1,4 +1,4 @@
-session HOL! in "." = Pure +
+session HOL! (main) in "." = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
@@ -19,8 +19,8 @@
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! in "." = Pure +
-  description {* HOL-Main with proof terms *}
+session "HOL-Proofs"! (main) in "." = Pure +
+  description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
 
@@ -571,7 +571,7 @@
     "ex/Koepf_Duermuth_Countermeasure"
   files "document/root.tex"
 
-session Nominal = HOL +
+session Nominal (main) = HOL +
   options [document = false]
   theories Nominal
 
@@ -760,7 +760,7 @@
     Predicate_Compile_Tests
     Specialisation_Examples
 
-session HOLCF! = HOL +
+session HOLCF! (main) = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman