Structured Presentation of Formal Proofs: an Experiment with Isabelle (2009)
F. Kammüller, G. Keller, M. Simons, M. Weber, Tu Berlin
The intelligible presentation of formal proofs is usually not attempted because of their technical detail. This formal noise hides the line of reasoning that can be followed and understood by humans....