src/HOL/ROOT

-session HOL! (1) in "." = Pure +
+session HOL! in "." = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
   files "document/root.bib" "document/root.tex"
 

 session "HOL-Main"! in "." = Pure +
   description {* HOL side-entry for Main only, without Complex_Main *}
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! (4) in "." = Pure +
+session "HOL-Proofs"! in "." = Pure +
   description {* HOL-Main with proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
 
 session Library = HOL +

     Probability
     "ex/Dining_Cryptographers"
     "ex/Koepf_Duermuth_Countermeasure"
   files "document/root.tex"
 
-session Nominal (2) = HOL +
+session Nominal = HOL +
   options [document = false]
   theories Nominal
 
 session Examples in "Nominal/Examples" = "HOL-Nominal" +
   options [condition = ISABELLE_POLYML, document = false]

   theories  (* FIXME *)
     Examples
     Predicate_Compile_Tests
     Specialisation_Examples
 
-session HOLCF! (3) = HOL +
+session HOLCF! = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
 
     HOLCF -- a semantic extension of HOL by the LCF logic.