Isabelle Packages

Isabelle Distribution Area

Isabelle Packages

The following source and binary packages of Isabelle2002 provide everything required for easy installation of the full Isabelle working environment on common Unix platforms.

A minimal Isabelle installation requires only bash and perl (usually provided by the operating system), and a suitable implementation of Standard ML (e.g. Poly/ML as included below). A comfortable Isabelle working environment demands further user interface support, as provided by Proof General (please register) together with the (optional) X-Symbol package. Both of these should be used with a recent version of XEmacs-21 (preferably with MULE).

Packages

We provide a complete set of packages for Isabelle, Proof General and X-Symbol. While XEmacs-21 is not included here, most operating system distributions already provide a suitable package, although not installed by default. Some of the packages below are platform dependent; we include binaries for Linux/x86, Solaris/Sparc, and Darwin/PPC (MacOS X).

Isabelle
Sources and documentation	Isabelle2002.tar.gz	4578 K
Documentation in PDF	Isabelle2002_pdf.tar.gz	4066 K
Theory library in PDF and HTML	Isabelle2002_library.tar.gz	9633 K
Proof General
Proof General	ProofGeneral.tar.gz	710 K
X-Symbol package	x-symbol.tar.gz	454 K
Poly/ML compiler and runtime system
Poly/ML base system	polyml_base.tar.gz	2 K
Poly/ML binary modules	polyml_x86-linux.tar.gz	1287 K
	polyml_sparc-solaris.tar.gz	2307 K
	polyml_ppc-darwin.tar.gz	1461 K
Precompiled logics
HOL	HOL_x86-linux.tar.gz	6429 K
	HOL_sparc-solaris.tar.gz	7227 K
	HOL_ppc-darwin.tar.gz	7073 K
HOL-Real	HOL-Real_x86-linux.tar.gz	7037 K
	HOL-Real_sparc-solaris.tar.gz	7925 K
	HOL-Real_ppc-darwin.tar.gz	7749 K
ZF	ZF_x86-linux.tar.gz	5617 K
	ZF_sparc-solaris.tar.gz	6284 K
	ZF_ppc-darwin.tar.gz	6159 K

Installation

In fact, there is no installation required. Users may just unpack all required packages within the same directory. The default settings of Isabelle should be reasonable for most circumstances.

A typical Linux/x86 site installation of Isabelle/HOL works as follows. By using GNU tar, the archives are uncompressed and unpacked into the /usr/local directory (this location may be changed to anything appropriate).

tar -C /usr/local -xzf Isabelle2002.tar.gz tar -C /usr/local -xzf ProofGeneral.tar.gz tar -C /usr/local -xzf x-symbol.tar.gz tar -C /usr/local -xzf polyml_base.tar.gz tar -C /usr/local -xzf polyml_x86-linux.tar.gz tar -C /usr/local -xzf HOL_x86-linux.tar.gz

Users may now invoke Isabelle without further ado, e.g. run the main executable /usr/local/Isabelle/bin/Isabelle to launch the Proof General interface for Isabelle/Isar. Note that there is a separate option to enable X-Symbol.

last update at 03/08/2002