README

updated for Isabelle94

		     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.  The command
	conv-theory-files.pl | grep mv
generates commands to rename all theory files in a directory hierarchy.  
------------------------------------------------------------------------------

This directory contains the complete Isabelle system.  To build and test the
entire system, including all object-logics, use the shell script make-all.
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 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

The directory Pure containes pure Isabelle, which has no object-logic.

Other important files include...
  COPYRIGHT   		Copyright notice and Disclaimer of Warranty
  make-all		shell script for building entire system
  make-all-poly		sample make-all invocation for Poly/ML
  make-all-nj		sample make-all invocation for SML of NJ
  change_simp		shell script to help convert sources to new simplifier
  conv-theory-files.pl  perl script to rename old theory files
  expandshort		shell script to expand "shortcuts" in files
  prove_goal.el       	Emacs command to change proof format
  xlisten		shell script for running Isabelle under X
  teeinput		shell script to run Isabelle, logging inputs to a file
  Pure			directory of source files for Pure Isabelle
  Provers		directory of generic theorem provers

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.

A *very* primitive alternative, xlisten sets up a window running Isabelle,
with a separate small "listener" window, which keeps a log of all input
lines.  If you are not running the X Window System, teeinput can still be
used to record the log.

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

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 <[e-mail]> at Abstract
Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
England.

To obtain Standard ML of New Jersey, contact David MacQueen
<[e-mail]> 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 [e-mail] provides a forum
for Isabelle users to discuss problems and exchange information.  To join,
send a message to [e-mail].

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

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: [e-mail]
Computer Laboratory 		Phone: [phone]
University of Cambridge 	Fax:   [phone] 
Pembroke Street 
Cambridge CB2 3QG 
England

Tobias Nipkow			E-mail: [e-mail]
Institut für Informatik		Phone: [phone]
T. U. München			Fax:   [phone]
D-80290 München
Germany

$Id$