src/HOL/ROOT
author wenzelm
Tue Jul 24 12:38:33 2012 +0200 (2012-07-24)
changeset 48470 7483aa690b4f
parent 48458 09710d6fc3d1
child 48481 2c828c830ad7
permissions -rw-r--r--
clarified "document" again, eliminated redundant "no_document";
wenzelm@48349
     1
session HOL! (1) in "." = Pure +
wenzelm@48338
     2
  description {* Classical Higher-order Logic *}
wenzelm@48338
     3
  options [document_graph]
wenzelm@48338
     4
  theories Complex_Main
wenzelm@48338
     5
  files "document/root.tex" "document/root.bib"
wenzelm@48338
     6
wenzelm@48338
     7
session "HOL-Base"! in "." = Pure +
wenzelm@48338
     8
  description {* Raw HOL base, with minimal tools *}
wenzelm@48470
     9
  options [document = false]
wenzelm@48338
    10
  theories HOL
wenzelm@48338
    11
wenzelm@48338
    12
session "HOL-Plain"! in "." = Pure +
wenzelm@48338
    13
  description {* HOL side-entry after bootstrap of many tools and packages *}
wenzelm@48470
    14
  options [document = false]
wenzelm@48338
    15
  theories Plain
wenzelm@48338
    16
wenzelm@48338
    17
session "HOL-Main"! in "." = Pure +
wenzelm@48338
    18
  description {* HOL side-entry for Main only, without Complex_Main *}
wenzelm@48470
    19
  options [document = false]
wenzelm@48338
    20
  theories Main
wenzelm@48338
    21
wenzelm@48349
    22
session "HOL-Proofs"! (2) in "." = Pure +
wenzelm@48338
    23
  description {* HOL-Main with proof terms *}
wenzelm@48470
    24
  options [document = false, proofs = 2, parallel_proofs = 0]
wenzelm@48338
    25
  theories Main
wenzelm@48338
    26
wenzelm@48349
    27
session HOLCF! (3) = HOL +
wenzelm@48338
    28
  description {*
wenzelm@48338
    29
    Author:     Franz Regensburger
wenzelm@48338
    30
    Author:     Brian Huffman
wenzelm@48338
    31
wenzelm@48338
    32
    HOLCF -- a semantic extension of HOL by the LCF logic.
wenzelm@48338
    33
  *}
wenzelm@48338
    34
  options [document_graph]
wenzelm@48470
    35
  theories [document = false]
wenzelm@48338
    36
    "~~/src/HOL/Library/Nat_Bijection"
wenzelm@48338
    37
    "~~/src/HOL/Library/Countable"
wenzelm@48338
    38
  theories Plain_HOLCF Fixrec HOLCF
wenzelm@48338
    39
  files "document/root.tex"
wenzelm@48338
    40