Isabelle/Isar --- a versatile environment for human-readable formal proof documents
Markus Wenzel · 2002
The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logical foundations of Isar are achieved by interpretation within the generic Natural Deduction framework of Isabelle, reducing all high-level reasoning steps to primitive inferences. The resulting Isabelle/Isar system...