src/HOL/ROOT
changeset 48458 09710d6fc3d1
parent 48421 c4d337782de4
child 48470 7483aa690b4f
equal deleted inserted replaced
48457:fd9e28d5a143 48458:09710d6fc3d1
     4   theories Complex_Main
     4   theories Complex_Main
     5   files "document/root.tex" "document/root.bib"
     5   files "document/root.tex" "document/root.bib"
     6 
     6 
     7 session "HOL-Base"! in "." = Pure +
     7 session "HOL-Base"! in "." = Pure +
     8   description {* Raw HOL base, with minimal tools *}
     8   description {* Raw HOL base, with minimal tools *}
     9   options [document = false]
     9   options [no_document]
    10   theories HOL
    10   theories HOL
    11 
    11 
    12 session "HOL-Plain"! in "." = Pure +
    12 session "HOL-Plain"! in "." = Pure +
    13   description {* HOL side-entry after bootstrap of many tools and packages *}
    13   description {* HOL side-entry after bootstrap of many tools and packages *}
    14   options [document = false]
    14   options [no_document]
    15   theories Plain
    15   theories Plain
    16 
    16 
    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 [no_document]
    20   theories Main
    20   theories Main
    21 
    21 
    22 session "HOL-Proofs"! (2) in "." = Pure +
    22 session "HOL-Proofs"! (2) 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 [no_document, proofs = 2, parallel_proofs = 0]
    25   theories Main
    25   theories Main
    26 
    26 
    27 session HOLCF! (3) = HOL +
    27 session HOLCF! (3) = HOL +
    28   description {*
    28   description {*
    29     Author:     Franz Regensburger
    29     Author:     Franz Regensburger
    30     Author:     Brian Huffman
    30     Author:     Brian Huffman
    31 
    31 
    32     HOLCF -- a semantic extension of HOL by the LCF logic.
    32     HOLCF -- a semantic extension of HOL by the LCF logic.
    33   *}
    33   *}
    34   options [document_graph]
    34   options [document_graph]
    35   theories [document = false]
    35   theories [no_document]
    36     "~~/src/HOL/Library/Nat_Bijection"
    36     "~~/src/HOL/Library/Nat_Bijection"
    37     "~~/src/HOL/Library/Countable"
    37     "~~/src/HOL/Library/Countable"
    38   theories Plain_HOLCF Fixrec HOLCF
    38   theories Plain_HOLCF Fixrec HOLCF
    39   files "document/root.tex"
    39   files "document/root.tex"
    40 
    40