Technical reports
Introduction to Isabelle
January 1993, 61 pages
DOI: 10.48456/tr-280
Abstract
Isabelle is a generic theorem prover, supporting formal proof in a variety of logics. Through a variety of examples, this paper explains the basic theory demonstrates the most important commands. It serves as the introduction to other Isabelle documentation.
Full text
DVI (0.1 MB)
BibTeX record
@TechReport{UCAM-CL-TR-280, author = {Paulson, Lawrence C.}, title = {{Introduction to Isabelle}}, year = 1993, month = jan, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-280.dvi.gz}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-280}, number = {UCAM-CL-TR-280} }