src/HOL/ROOT
author wenzelm
Tue, 24 Jul 2012 10:11:49 +0200
changeset 48458 09710d6fc3d1
parent 48421 c4d337782de4
child 48470 7483aa690b4f
permissions -rw-r--r--
clarified document options;

session HOL! (1) in "." = Pure +
  description {* Classical Higher-order Logic *}
  options [document_graph]
  theories Complex_Main
  files "document/root.tex" "document/root.bib"

session "HOL-Base"! in "." = Pure +
  description {* Raw HOL base, with minimal tools *}
  options [no_document]
  theories HOL

session "HOL-Plain"! in "." = Pure +
  description {* HOL side-entry after bootstrap of many tools and packages *}
  options [no_document]
  theories Plain

session "HOL-Main"! in "." = Pure +
  description {* HOL side-entry for Main only, without Complex_Main *}
  options [no_document]
  theories Main

session "HOL-Proofs"! (2) in "." = Pure +
  description {* HOL-Main with proof terms *}
  options [no_document, proofs = 2, parallel_proofs = 0]
  theories Main

session HOLCF! (3) = HOL +
  description {*
    Author:     Franz Regensburger
    Author:     Brian Huffman

    HOLCF -- a semantic extension of HOL by the LCF logic.
  *}
  options [document_graph]
  theories [no_document]
    "~~/src/HOL/Library/Nat_Bijection"
    "~~/src/HOL/Library/Countable"
  theories Plain_HOLCF Fixrec HOLCF
  files "document/root.tex"