src/HOL/ROOT
changeset 48338 3592a2091c80
child 48349 a78e5d399599
equal deleted inserted replaced
48337:9c7f8e5805b4 48338:3592a2091c80
       
     1 session HOL! in "." = Pure +
       
     2   description {* Classical Higher-order Logic *}
       
     3   options [document_graph]
       
     4   theories Complex_Main
       
     5   files "document/root.tex" "document/root.bib"
       
     6 
       
     7 session "HOL-Base"! in "." = Pure +
       
     8   description {* Raw HOL base, with minimal tools *}
       
     9   options [document = false]
       
    10   theories HOL
       
    11 
       
    12 session "HOL-Plain"! in "." = Pure +
       
    13   description {* HOL side-entry after bootstrap of many tools and packages *}
       
    14   options [document = false]
       
    15   theories Plain
       
    16 
       
    17 session "HOL-Main"! in "." = Pure +
       
    18   description {* HOL side-entry for Main only, without Complex_Main *}
       
    19   options [document = false]
       
    20   theories Main
       
    21 
       
    22 session "HOL-Proofs"! in "." = Pure +
       
    23   description {* HOL-Main with proof terms *}
       
    24   options [document = false, proofs = 2, parallel_proofs = false]
       
    25   theories Main
       
    26 
       
    27 session HOLCF! = HOL +
       
    28   description {*
       
    29     Author:     Franz Regensburger
       
    30     Author:     Brian Huffman
       
    31 
       
    32     HOLCF -- a semantic extension of HOL by the LCF logic.
       
    33   *}
       
    34   options [document_graph]
       
    35   theories [document = false]
       
    36     "~~/src/HOL/Library/Nat_Bijection"
       
    37     "~~/src/HOL/Library/Countable"
       
    38   theories Plain_HOLCF Fixrec HOLCF
       
    39   files "document/root.tex"
       
    40