README
changeset 0 a5a9c433f639
child 86 3406bd994306
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/README	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,113 @@
     1.4 +		     ISABELLE-92 DISTRIBUTION DIRECTORY
     1.5 +
     1.6 +------------------------------------------------------------------------------
     1.7 +ISABELLE-92 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
     1.8 +DOCUMENTATION.
     1.9 +------------------------------------------------------------------------------
    1.10 +
    1.11 +This directory contains the complete Isabelle system.  To build and test the
    1.12 +entire system, including all object-logics, use the shell script make-all.
    1.13 +Pure Isabelle and each of the object-logics can be built separately using the
    1.14 +Makefiles in the respective directories; read them for more information.
    1.15 +
    1.16 +				THE MAKEFILES
    1.17 +
    1.18 +The Makefiles can use two different Standard ML compilers: Poly/ML version
    1.19 +1.88MSX or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
    1.20 +(Version 75 or later).  Poly/ML is a commercial product and costs money,
    1.21 +but it is reliable and its database system is convenient for interactive
    1.22 +work.  SML of New Jersey requires lots of memory and disc space, but it is
    1.23 +free and its code sometimes runs faster.  Both compilers are perfectly
    1.24 +satisfactory for running Isabelle.
    1.25 +
    1.26 +The Makefiles and make-all use enviroment variables that you should set
    1.27 +according to your site configuration.
    1.28 +
    1.29 +ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    1.30 +images.  When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
    1.31 +starting with "/").
    1.32 +
    1.33 +ML_DBASE is an absolute pathname to the initial Poly/ML database (not
    1.34 +required for New Jersey ML).
    1.35 +
    1.36 +ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
    1.37 +ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
    1.38 +it is Poly/ML; if it begins with the letters "sml" then they assume
    1.39 +Standard ML of New Jersey.
    1.40 +
    1.41 +
    1.42 +			 STRUCTURE OF THIS DIRECTORY
    1.43 +
    1.44 +The directory Pure containes pure Isabelle, which has no object-logic.
    1.45 +
    1.46 +Other important files include...
    1.47 +    COPYRIGHT   	Copyright notice and Disclaimer of Warranty
    1.48 +    make-rulenames	shell script used during Make
    1.49 +    make-all		shell script for building entire system
    1.50 +    expandshort		shell script to expand "shortcuts" in files
    1.51 +    prove_goal.el       Emacs command to change proof format
    1.52 +    xlisten		shell script for running Isabelle under X
    1.53 +    teeinput		shell script to run Isabelle, logging inputs to a file
    1.54 +    theory-template.ML	template file for defining new theories
    1.55 +    Pure		directory of source files for Pure Isabelle
    1.56 +    Provers		directory of generic theorem provers
    1.57 +
    1.58 +xlisten sets up a window running Isabelle, with a separate small "listener"
    1.59 +window, which keeps a log of all input lines.  This log is a useful record
    1.60 +of a session.  If you are not running X windows, teeinput can still be used at
    1.61 +least to record (if not to display) the log.
    1.62 +
    1.63 +The following subdirectories contain object-logics:
    1.64 +    FOL 	Natural deduction logic (intuitionistic and classical)
    1.65 +    ZF		Zermelo-Fraenkel Set theory
    1.66 +    CTT		Constructive Type Theory
    1.67 +    HOL		Classical Higher-Order Logic
    1.68 +    LK		Classical sequent calculus
    1.69 +    Modal	The modal logics T, S4, S43
    1.70 +    LCF         Logic for Computable Functions (domain theory)
    1.71 +    Cube	Barendregt's Lambda Cube
    1.72 +
    1.73 +Object-logics include examples files in subdirectory ex or file ex.ML.
    1.74 +These files can be loaded in batch mode.  The commands can also be
    1.75 +executed interactively, using the windows on your workstation.  This is a
    1.76 +good way to get started.
    1.77 +
    1.78 +Each object-logic is built on top of Pure Isabelle, and possibly on top of
    1.79 +another object logic (like FOL or LK).  A database or binary called Pure is
    1.80 +first created, then the object-logic is loaded on top.  Poly/ML extends
    1.81 +Pure using its "make_database" operation.  Standard ML of New Jersey starts
    1.82 +with the Pure core image and loads the object-logic's ROOT.ML.
    1.83 +
    1.84 +		HOW TO GET A STANDARD ML COMPILER
    1.85 +
    1.86 +To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
    1.87 +Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
    1.88 +England.
    1.89 +
    1.90 +To obtain Standard ML of New Jersey, contact David MacQueen
    1.91 +<dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
    1.92 +Murray Hill, NJ 07974, USA.  This compiler is available by FTP.  Connect to
    1.93 +research.att.com; login as anonymous with your userid as password; set
    1.94 +binary mode; transfer files from the directory dist/ml.
    1.95 +
    1.96 +------------------------------------------------------------------------------
    1.97 +
    1.98 +Please report any problems you encounter.  While we will try to be helpful,
    1.99 +we can accept no responsibility for the deficiences of Isabelle amd their
   1.100 +consequences.
   1.101 +
   1.102 +Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
   1.103 +Computer Laboratory 		Phone: +44-223-334600
   1.104 +University of Cambridge 	Fax:   +44-223-334748 
   1.105 +Pembroke Street 
   1.106 +Cambridge CB2 3QG 
   1.107 +England
   1.108 +
   1.109 +Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   1.110 +Institut fuer Informatik	Phone: +49-89-2105-2690
   1.111 +T. U. Muenchen			Fax:   +49-89-2105-8183
   1.112 +Postfach 20 24 20
   1.113 +D-8000 Muenchen 2
   1.114 +Germany
   1.115 +
   1.116 +Last updated 25 August 1992