src/Pure/ROOT
author wenzelm
Mon, 20 May 2024 15:43:51 +0200
changeset 80182 29f2b8ff84f3
parent 74836 a97ec0954c50
permissions -rw-r--r--
proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f);

chapter Pure

session Pure =
  description "
    The Pure logical framework.
  "
  options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false]
  theories [export_theory]
    Pure (global)
  theories
    ML_Bootstrap (global)
    Sessions

session "Pure-Examples" in Examples = Pure +
  description "
    Notable Examples for Isabelle/Pure.
  "
  theories
    First_Order_Logic
    Higher_Order_Logic
  document_files
    "root.bib"
    "root.tex"

session "Pure-ex" in ex = Pure +
  description "
    Miscellaneous examples and experiments for Isabelle/Pure.
  "
  options [document_heading_prefix = ""]
  sessions
    "Pure-Examples"
  theories [document = false]
    Def
    Def_Examples
    Guess
    Guess_Examples
  theories
    Alternative_Headings
    Alternative_Headings_Examples
  document_files
    "root.tex"