src/HOL/ROOT
changeset 48487 94a9650f79fb
parent 48486 691d0b44a793
child 48492 03530cf284ca
equal deleted inserted replaced
48486:691d0b44a793 48487:94a9650f79fb
    17 session "HOL-Main"! in "." = Pure +
    17 session "HOL-Main"! in "." = Pure +
    18   description {* HOL side-entry for Main only, without Complex_Main *}
    18   description {* HOL side-entry for Main only, without Complex_Main *}
    19   options [document = false]
    19   options [document = false]
    20   theories Main
    20   theories Main
    21 
    21 
    22 session "HOL-Proofs"! (2) in "." = Pure +
    22 session "HOL-Proofs"! (4) in "." = Pure +
    23   description {* HOL-Main with proof terms *}
    23   description {* HOL-Main with proof terms *}
    24   options [document = false, proofs = 2, parallel_proofs = 0]
    24   options [document = false, proofs = 2, parallel_proofs = 0]
    25   theories Main
    25   theories Main
    26 
    26 
    27 session Library = HOL +
    27 session Library = HOL +
   568     Probability
   568     Probability
   569     "ex/Dining_Cryptographers"
   569     "ex/Dining_Cryptographers"
   570     "ex/Koepf_Duermuth_Countermeasure"
   570     "ex/Koepf_Duermuth_Countermeasure"
   571   files "document/root.tex"
   571   files "document/root.tex"
   572 
   572 
   573 session Nominal = HOL +
   573 session Nominal (2) = HOL +
   574   options [document = false]
   574   options [document = false]
   575   theories Nominal
   575   theories Nominal
   576 
   576 
   577 session Examples in "Nominal/Examples" = "HOL-Nominal" +
   577 session Examples in "Nominal/Examples" = "HOL-Nominal" +
   578   options [document = false]
   578   options [document = false]