README.old

Deleted option_case_tac because exhaust_tac performs a similar function.

Deleted the duplicate proof of expand_option_case...

***************************************************************************

IMPORTANT NOTE: This is the old README. The installation procedure
described below basically still works for Isabelle94-8, but will be
phased out next time.

***************************************************************************



		     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.

			HOW TO BUILD ISABELLE

Here are brief instructions.  For more detail, read further.

1.  Create a directory to hold the Isabelle executable images.
    Set the environment variable ISABELLEBIN to its full (absolute) pathname.

2.  Set the environment variable ISABELLECOMP to the command to execute your
    Standard ML compiler.

3.  If using Poly/ML, set the environment variable ML_DBASE to the full 
    pathname of the empty Poly/ML database.

4.  Change your working directory to that containing this file.

5a. To build ALL logics and run examples, type "make-all" and wait up to 
    10 hours.  Standard ML of New Jersey will require up to 200M
    of disc space!  Poly/ML will require about 25M.

-OR-
5b. To build ALL logics but run no examples, type "make-all -notest".  This
    is much faster than 5a but needs just as much disc space.

-OR-
5c. To build just one logic, such as HOL, change to directory HOL and type
    "make" or "make test".  This may trigger further Makes automatically.


			SUITABLE ML COMPILERS

You 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 stable and
efficient; moreover its database system is convenient for interactive work.
SML/NJ needs lots of store and disc space, but it is free.  Some recent
versions of SML/NJ are significantly faster than 0.93, but beware of many
incompatibilities among them; you might be forced to edit the file
Pure/NJ1xx.ML.  VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW.

To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
University, Uxbridge UB8 3PH, England, email [e-mail].

To obtain Standard ML of New Jersey, see the Web page 
	http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
or send email to [e-mail].


			ENVIRONMENT VARIABLES

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.  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 command to run ML compiler, typically "/bin/sml" or "poly
-noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
allocation, which you should consider increasing if a command fails with the
message "Run out of store".)  Please DO NOT use a command such as
"sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the
Makefiles. 

If, after stripping a leading pathname, the compiler begins with the letters
"poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
then they assume Standard ML of New Jersey.


			 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.
  Tools		contains shell scripts and utilities 

The following subdirectories contain object-logics:
  FOL 		natural deduction First-Order Logic 
			(intuitionistic and classical versions)
  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
  Sequents	Sequent calcul: first-order logic
				modal logics T, S4, S43
				intuitionistic linear logic
  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 HOL.  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.

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

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$