Technical reports

Introduction to Isabelle

Lawrence C. Paulson

January 1993, 61 pages

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 = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-280.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-280}
}