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