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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48349
a78e5d399599 support Session.Queue with ordering and dependencies;
wenzelm
parents: 48338
diff changeset
     1
session HOL! (1) in "." = Pure +
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     2
  description {* Classical Higher-order Logic *}
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     3
  options [document_graph]
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     4
  theories Complex_Main
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     5
  files "document/root.tex" "document/root.bib"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     6
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     7
session "HOL-Base"! in "." = Pure +
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     8
  description {* Raw HOL base, with minimal tools *}
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48421
diff changeset
     9
  options [no_document]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    10
  theories HOL
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    11
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    12
session "HOL-Plain"! in "." = Pure +
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    13
  description {* HOL side-entry after bootstrap of many tools and packages *}
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48421
diff changeset
    14
  options [no_document]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    15
  theories Plain
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    16
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    17
session "HOL-Main"! in "." = Pure +
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    18
  description {* HOL side-entry for Main only, without Complex_Main *}
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48421
diff changeset
    19
  options [no_document]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    20
  theories Main
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    21
48349
a78e5d399599 support Session.Queue with ordering and dependencies;
wenzelm
parents: 48338
diff changeset
    22
session "HOL-Proofs"! (2) in "." = Pure +
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    23
  description {* HOL-Main with proof terms *}
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48421
diff changeset
    24
  options [no_document, proofs = 2, parallel_proofs = 0]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    25
  theories Main
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    26
48349
a78e5d399599 support Session.Queue with ordering and dependencies;
wenzelm
parents: 48338
diff changeset
    27
session HOLCF! (3) = HOL +
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    28
  description {*
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    29
    Author:     Franz Regensburger
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    30
    Author:     Brian Huffman
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    31
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    32
    HOLCF -- a semantic extension of HOL by the LCF logic.
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    33
  *}
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    34
  options [document_graph]
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48421
diff changeset
    35
  theories [no_document]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    36
    "~~/src/HOL/Library/Nat_Bijection"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    37
    "~~/src/HOL/Library/Countable"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    38
  theories Plain_HOLCF Fixrec HOLCF
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    39
  files "document/root.tex"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    40