Computer Laboratory

Technical reports

Introduction to Isabelle

Lawrence C. Paulson

January 1993, 61 pages


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

  author =	 {Paulson, Lawrence C.},
  title = 	 {{Introduction to Isabelle}},
  year = 	 1993,
  month = 	 jan,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-280}