|
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
|