1 ISABELLE-93 DISTRIBUTION DIRECTORY
3 ------------------------------------------------------------------------------
4 ISABELLE-93 IS INCOMPATIBLE WITH EARLIER VERSIONS. PLEASE CONSULT THE
6 ------------------------------------------------------------------------------
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.
15 The Makefiles can use two different Standard ML compilers: Poly/ML version
16 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
17 (Version 0.93 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 store and disc space, but it is
20 free and its code sometimes runs faster. Both compilers are perfectly
21 satisfactory for running Isabelle.
23 The Makefiles and make-all use enviroment variables that you should set
24 according to your site configuration.
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
30 ML_DBASE is an *absolute* pathname to the initial Poly/ML database (not
31 required for New Jersey ML).
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.
38 If a Poly/ML session fails with the message "Run out of store" then you
39 have used up the entire heap. If your tactic is not in a loop, allocating
40 more heap at startup should correct the problem. For instance, "poly -h
41 15000" allocates sufficient heap space to rebuild all Isabelle examples.
44 STRUCTURE OF THIS DIRECTORY
46 The directory Pure containes pure Isabelle, which has no object-logic.
48 Other important files include...
49 COPYRIGHT Copyright notice and Disclaimer of Warranty
50 make-all shell script for building entire system
51 change_simp shell script to help convert sources to new simplifier
52 expandshort shell script to expand "shortcuts" in files
53 prove_goal.el Emacs command to change proof format
54 xlisten shell script for running Isabelle under X
55 teeinput shell script to run Isabelle, logging inputs to a file
56 Pure directory of source files for Pure Isabelle
57 Provers directory of generic theorem provers
59 xlisten sets up a window running Isabelle, with a separate small "listener"
60 window, which keeps a log of all input lines. This log is a useful record
61 of a session. If you are not running X windows, teeinput can still be used at
62 least to record (if not to display) the log.
64 The following subdirectories contain object-logics:
65 FOL Natural deduction First-Order Logic (intuitionistic and classical)
66 FOLP First-Order Logic with Proof terms
67 ZF Zermelo-Fraenkel set theory
68 CTT Constructive Type Theory
69 HOL Classical Higher-Order Logic
70 LK Classical first-order sequent calculus
71 Modal The modal logics T, S4, S43
72 LCF Logic for Computable Functions (domain theory)
73 CCL Martin Coen's Classical Computational Logic
74 Cube Barendregt's Lambda Cube
76 Object-logics include examples files in subdirectory ex or file ex.ML.
77 These files can be loaded in batch mode. The commands can also be
78 executed interactively, using the windows on your workstation. This is a
79 good way to get started.
81 Each object-logic is built on top of Pure Isabelle, and possibly on top of
82 another object logic like FOL or LK. A database or binary called Pure is
83 first created, then the object-logic is loaded on top. Poly/ML extends
84 Pure using its "make_database" operation. Standard ML of New Jersey starts
85 with the Pure core image and loads the object-logic's ROOT.ML.
87 HOW TO GET A STANDARD ML COMPILER
89 To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
90 Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
93 To obtain Standard ML of New Jersey, contact David MacQueen
94 <dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
95 Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to
96 research.att.com; login as anonymous with your userid as password; set
97 binary mode; transfer files from the directory dist/ml.
99 ------------------------------------------------------------------------------
101 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
102 for Isabelle users to discuss problems and exchange information. To join,
103 send a message to isabelle-users-request@cl.cam.ac.uk.
105 ------------------------------------------------------------------------------
107 Please report any problems you encounter. While we shall try to be helpful,
108 we can accept no responsibility for the deficiences of Isabelle and their
111 Lawrence C Paulson E-mail: lcp@cl.cam.ac.uk
112 Computer Laboratory Phone: +44-223-334600
113 University of Cambridge Fax: +44-223-334748
118 Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de
119 Institut fuer Informatik Phone: +49-89-2105-2690
120 T. U. Muenchen Fax: +49-89-2105-8183
124 Last updated 13 December 1993