Experience with Isabelle A generic theorem prover
Lawrence Charles Paulson · OpenGrey (Institut de l'Information Scientifique et Technique) · 2021
The theorem prover Isabelle is described briefly and informally. Its historical development is traced from Edinburgh LCF to the present day. The main issues are unification, quantifiers, and the representation of inference rules. The Edinburgh Logical Framework is also described, for a comparison with Isabelle. An appendix presents several Isabelle logics, including set theory and Constructive Type Theory, with examples of theorems.