An approach to literate and structured formal developments

We present an approach to the literate and structured presentation of formal developments. We discuss the presentation of formal developments in a logical framework and distinguish three aspects: language-related aspects, structural aspects of proofs, and presentational aspects. We illustrate the approach by two examples: a simple mathematical proof of the Knaster-Tarski fixpoint theorem, and a formalization of the VDM development of a revision management system.