Department of Computer Science and Technology

Technical reports

Experience with Isabelle
A generic theorem prover

Lawrence C. Paulson

August 1988, 20 pages


The theorem prover Isabelle is described briefly and informally. Its historical development is traced from Edinburgh LCF to the present day. The main issues are unification, quantifiers, and the representation of inference rules. The Edinburgh Logical Framework is also described, for a comparison with Isabelle. An appendix presents several Isabelle logics, including set theory and Constructive Type Theory, with examples of theorems.

Full text

PDF (0.2 MB)
DVI (0.0 MB)

BibTeX record

  author =	 {Paulson, Lawrence C.},
  title = 	 {{Experience with Isabelle : A generic theorem prover}},
  year = 	 1988,
  month = 	 aug,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-143}