Abstract. We present a generic approach to readable formal proof documents, called Intelligible semi-automated reasoning (Isar). It addresses the major problem of existing interact...
g to the well-known “LCF approach” of secure inferences as abstract datatype constructors in ML [16]; explicit proof terms are also available [8]. Isabelle/Isar provides sophis...
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipko...