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...
The standard versions of HOL only support disjoint sums over finite families of types. This paper introduces disjoint sums over type classes containing possibly a countably infinit...
Abstract. We describe the key features of the proof description language of Declare, an experimental theorem prover for higher order logic. We take a somewhat radical approach to p...