src/HOL/ROOT

     "ex/Dining_Cryptographers"
     "ex/Koepf_Duermuth_Countermeasure"
     "ex/Measure_Not_CCC"
   document_files "root.tex"
 
-session "HOL-Nominal" (main) in Nominal = HOL +
+session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
   theories Nominal
 
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   options [condition = ML_SYSTEM_POLYML, document = false]