Technical reports
Isabelle tutorial and user’s manual
Lawrence C. Paulson, Tobias Nipkow
January 1990, 142 pages
DOI: 10.48456/tr-189
Abstract
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.
Full text
BibTeX record
@TechReport{UCAM-CL-TR-189,
author = {Paulson, Lawrence C. and Nipkow, Tobias},
title = {{Isabelle tutorial and user's manual}},
year = 1990,
month = jan,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-189.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-189},
number = {UCAM-CL-TR-189}
}