A preliminary users manual for Isabelle
Lawrence Charles Paulson · OpenGrey (Institut de l'Information Scientifique et Technique) · 2021
This is an early report on the theorem prover Isabelle and several of its object-logics. It describes Isabelle’s operations, commands, data structures, and organization. This information is fairly low-level, but could benefit Isabelle users and implementors of other systems.