src/Pure/ROOT

more informative errors: simplify diagnosis of spurious failures reported by users;

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 in Isabelle/Pure.
  "
  theories
    First_Order_Logic
    Higher_Order_Logic
  document_files
    "root.bib"
    "root.tex"