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