ISABELLE-94 DISTRIBUTION DIRECTORY

------------------------------------------------------------------------------

ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE

DOCUMENTATION.  

In particular, theory files are no longer forced into lower case, but must

be identical to the actual theory name.  See the script

conv-theory-files.pl on directory Tools.

------------------------------------------------------------------------------

This directory contains the complete Isabelle system.  To build and test

all the Isabelle object-logics, use the shell script make-all (on directory

Tools).  Pure Isabelle and each of the object-logics can be built

separately using the Makefiles in the respective directories; read them for

more information.

				THE MAKEFILES

The Makefiles can use two different Standard ML compilers: Poly/ML version

2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey

(Version 0.93 or later).  Poly/ML is a commercial product and costs money,

but it is reliable and its database system is convenient for interactive

work.  SML of New Jersey requires lots of store and disc space, but it is

free and its code sometimes runs faster.  Both compilers are perfectly

satisfactory for running Isabelle.

The Makefiles and make-all use environment variables that you should set

according to your site configuration.  See file Tools/make-all-nj for an

example using the Bourne shell, sh.

ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML

images.  This directory *must* be different from the Isabelle source

directory.  When using Poly/ML, ISABELLEBIN must be an absolute pathname

(one starting with "/").

ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not

required for New Jersey ML.

ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If

ISABELLECOMP begins with the letters "poly" then the Makefiles assume that

it is Poly/ML; if it begins with the letters "sml" then they assume

Standard ML of New Jersey.  

If a Poly/ML session fails with the message "Run out of store" then you

have used up the entire heap.  If your tactic is not in a loop, allocating

more heap at startup should correct the problem.  For instance, "poly -h

15000" allocates sufficient heap space to rebuild all Isabelle examples.

			 STRUCTURE OF THIS DIRECTORY

Important files include...

  COPYRIGHT 	Copyright notice and Disclaimer of Warranty

  Pure		contains source files for Pure Isabelle (no object-logic)

  Provers	contains generic theorem provers: simplifier, etc.

The following subdirectories contain object-logics:

  FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)

  FOLP 	  First-Order Logic with Proof terms

  ZF	  Zermelo-Fraenkel set theory

  HOL	  Classical Higher-Order Logic

  LCF     Logic for Computable Functions (domain theory) built upon FOL

  HOLCF   A version of LCF built upon HOL

  CTT	  Constructive Type Theory

  LK	  Classical first-order sequent calculus

  Modal	  The modal logics T, S4, S43

  CCL	  Martin Coen's Classical Computational Logic

  Cube	  Barendregt's Lambda Cube

David Aspinall has written a user interface for Isabelle.  It runs under

GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp

from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.

Object-logics include examples files in subdirectory ex or file ex.ML.

These files can be loaded in batch mode.  The commands can also be

executed interactively, using the windows on your workstation.  This is a

good way to get started.

Each object-logic is built on top of Pure Isabelle, and possibly on top of

another object logic like FOL or LK.  A database or binary called Pure is

first created, then the object-logic is loaded on top.  Poly/ML extends

Pure using its "make_database" operation.  Standard ML of New Jersey starts

with the Pure core image and loads the object-logic's ROOT.ML.

		HOW TO GET A STANDARD ML COMPILER

To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract

Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,

England.

To obtain Standard ML of New Jersey, contact David MacQueen

<dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,

Murray Hill, NJ 07974, USA.  This compiler is available by FTP.  Connect to

research.att.com; login as anonymous with your userid as password; set

binary mode; transfer files from the directory dist/ml.

------------------------------------------------------------------------------

The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum

for Isabelle users to discuss problems and exchange information.  To join,

send a message to isabelle-users-request@cl.cam.ac.uk.

------------------------------------------------------------------------------

Please report any problems you encounter.  While we shall try to be helpful,

we can accept no responsibility for the deficiences of Isabelle and their

consequences.

Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk

Computer Laboratory 		Phone: +44-223-334600

University of Cambridge 	Fax:   +44-223-334748 

Pembroke Street 

Cambridge CB2 3QG 

England

Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de

Institut für Informatik		Phone: +49-89-2105-2690

T. U. München			Fax:   +49-89-2105-8183

D-80290 München

Germany

$Id$