chapter Pure session Pure = description {* The Pure logical framework *} global_theories Pure theories ML_Bootstrap