README
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 86 3406bd994306
permissions -rw-r--r--
Initial revision
     1 		     ISABELLE-92 DISTRIBUTION DIRECTORY
     2 
     3 ------------------------------------------------------------------------------
     4 ISABELLE-92 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
     5 DOCUMENTATION.
     6 ------------------------------------------------------------------------------
     7 
     8 This directory contains the complete Isabelle system.  To build and test the
     9 entire system, including all object-logics, use the shell script make-all.
    10 Pure Isabelle and each of the object-logics can be built separately using the
    11 Makefiles in the respective directories; read them for more information.
    12 
    13 				THE MAKEFILES
    14 
    15 The Makefiles can use two different Standard ML compilers: Poly/ML version
    16 1.88MSX or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
    17 (Version 75 or later).  Poly/ML is a commercial product and costs money,
    18 but it is reliable and its database system is convenient for interactive
    19 work.  SML of New Jersey requires lots of memory and disc space, but it is
    20 free and its code sometimes runs faster.  Both compilers are perfectly
    21 satisfactory for running Isabelle.
    22 
    23 The Makefiles and make-all use enviroment variables that you should set
    24 according to your site configuration.
    25 
    26 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    27 images.  When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
    28 starting with "/").
    29 
    30 ML_DBASE is an absolute pathname to the initial Poly/ML database (not
    31 required for New Jersey ML).
    32 
    33 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
    34 ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
    35 it is Poly/ML; if it begins with the letters "sml" then they assume
    36 Standard ML of New Jersey.
    37 
    38 
    39 			 STRUCTURE OF THIS DIRECTORY
    40 
    41 The directory Pure containes pure Isabelle, which has no object-logic.
    42 
    43 Other important files include...
    44     COPYRIGHT   	Copyright notice and Disclaimer of Warranty
    45     make-rulenames	shell script used during Make
    46     make-all		shell script for building entire system
    47     expandshort		shell script to expand "shortcuts" in files
    48     prove_goal.el       Emacs command to change proof format
    49     xlisten		shell script for running Isabelle under X
    50     teeinput		shell script to run Isabelle, logging inputs to a file
    51     theory-template.ML	template file for defining new theories
    52     Pure		directory of source files for Pure Isabelle
    53     Provers		directory of generic theorem provers
    54 
    55 xlisten sets up a window running Isabelle, with a separate small "listener"
    56 window, which keeps a log of all input lines.  This log is a useful record
    57 of a session.  If you are not running X windows, teeinput can still be used at
    58 least to record (if not to display) the log.
    59 
    60 The following subdirectories contain object-logics:
    61     FOL 	Natural deduction logic (intuitionistic and classical)
    62     ZF		Zermelo-Fraenkel Set theory
    63     CTT		Constructive Type Theory
    64     HOL		Classical Higher-Order Logic
    65     LK		Classical sequent calculus
    66     Modal	The modal logics T, S4, S43
    67     LCF         Logic for Computable Functions (domain theory)
    68     Cube	Barendregt's Lambda Cube
    69 
    70 Object-logics include examples files in subdirectory ex or file ex.ML.
    71 These files can be loaded in batch mode.  The commands can also be
    72 executed interactively, using the windows on your workstation.  This is a
    73 good way to get started.
    74 
    75 Each object-logic is built on top of Pure Isabelle, and possibly on top of
    76 another object logic (like FOL or LK).  A database or binary called Pure is
    77 first created, then the object-logic is loaded on top.  Poly/ML extends
    78 Pure using its "make_database" operation.  Standard ML of New Jersey starts
    79 with the Pure core image and loads the object-logic's ROOT.ML.
    80 
    81 		HOW TO GET A STANDARD ML COMPILER
    82 
    83 To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
    84 Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
    85 England.
    86 
    87 To obtain Standard ML of New Jersey, contact David MacQueen
    88 <dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
    89 Murray Hill, NJ 07974, USA.  This compiler is available by FTP.  Connect to
    90 research.att.com; login as anonymous with your userid as password; set
    91 binary mode; transfer files from the directory dist/ml.
    92 
    93 ------------------------------------------------------------------------------
    94 
    95 Please report any problems you encounter.  While we will try to be helpful,
    96 we can accept no responsibility for the deficiences of Isabelle amd their
    97 consequences.
    98 
    99 Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
   100 Computer Laboratory 		Phone: +44-223-334600
   101 University of Cambridge 	Fax:   +44-223-334748 
   102 Pembroke Street 
   103 Cambridge CB2 3QG 
   104 England
   105 
   106 Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   107 Institut fuer Informatik	Phone: +49-89-2105-2690
   108 T. U. Muenchen			Fax:   +49-89-2105-8183
   109 Postfach 20 24 20
   110 D-8000 Muenchen 2
   111 Germany
   112 
   113 Last updated 25 August 1992