Department of Computer Science and Technology

Technical reports

Isabelle tutorial and user’s manual

Lawrence C. Paulson, Tobias Nipkow

January 1990, 142 pages


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

PDF (0.5 MB)
DVI (0.1 MB)

BibTeX record

  author =	 {Paulson, Lawrence C. and Nipkow, Tobias},
  title = 	 {{Isabelle tutorial and user's manual}},
  year = 	 1990,
  month = 	 jan,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-189}