Use the mailing list
isabelleusers@cl.cam.ac.uk
for discussing problems and results. To subscribe,
contact our robot.
Isabelle is distributed under a BSDstyle open source licence.
To unpack a tar file such as Isabelle99.tar.gz
, use the command
tar zxf Isabelle99.tar.gz
 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 3540582444.
 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 ObjectLogics
that could not be included in the book.
These items are unsupported. But if you have any
success with them, please let me know.
 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 semanticsdirected compiler generator by
L. C. Paulson, POPL (1982) and in my
PhD Thesis.
It is sometimes called PSP in the literature. It is coded in ISO Pascal.
Last modified on $Date: 2004/04/20 11:41:45 $
Larry.Paulson@cl.cam.ac.uk
Back to Larry Paulson's Home Page