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