Use the mailing list
for discussing problems and results. To subscribe,
contact our robot.
Isabelle is distributed under a BSD-style open source licence.
To unpack a tar file such as
Isabelle99.tar.gz, use the command
tar zxf Isabelle99.tar.gz
These items are unsupported. But if you have any
success with them, please let me know.
- Isabelle: A Generic Theorem Prover.
By Lawrence C. Paulson, with contributions by Tobias Nipkow.
Springer Lecture Notes in Computer Science 828. XVII+321 pages, 1994.
Price: DM 66.00. ISBN 3-540-58244-4.
- Errata list.
Datatypes and (Co)Inductive Definitions in Isabelle/HOL,
by Tobias Nipkow and L. C. Paulson (1994).
Note: this consists of sections from Isabelle's Object-Logics
that could not be included in the book.
- The theorem prover Cambridge LCF. This is a
close predecessor of the Cambridge HOL system. It is documented in the
book Logic and Computation by L. C. Paulson (CUP, 1987). It is
coded in Franz Lisp.
- A very unusual compiler generator. It is
documented in A semantics-directed compiler generator by
L. C. Paulson, POPL (1982) and in my
It is sometimes called PSP in the literature. It is coded in ISO Pascal.
Last modified on $Date: 2004/04/20 11:41:45 $
Back to Larry Paulson's Home Page