Isabelle tutorial and user’s manual
Lawrence Charles Paulson, Tobias Nipkow · CL Technical Reports · 2021
This (obsolete!) manual describes how to use the theorem prover Isabelle. For beginners, it explains how to perform simple single-step proofs in the built-in logics. These include first-order logic, a classical sequent calculus, ZF set theory, Constructie Type Theory, and higher-order logic. Each of these logics is described. The manual then explains how to develop advanced tactics and tacticals and how to derive rules. Finally, it describes how to define new logics within Isabelle.