1 ISABELLE-94 DISTRIBUTION DIRECTORY
3 ------------------------------------------------------------------------------
4 ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS. PLEASE CONSULT THE
7 In particular, theory files are no longer forced into lower case, but must
8 be identical to the actual theory name. The command
9 conv-theory-files.pl | grep mv
10 generates commands to rename all theory files in a directory hierarchy.
11 ------------------------------------------------------------------------------
13 This directory contains the complete Isabelle system. To build and test the
14 entire system, including all object-logics, use the shell script make-all.
15 Pure Isabelle and each of the object-logics can be built separately using the
16 Makefiles in the respective directories; read them for more information.
20 The Makefiles can use two different Standard ML compilers: Poly/ML version
21 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
22 (Version 0.93 or later). Poly/ML is a commercial product and costs money,
23 but it is reliable and its database system is convenient for interactive
24 work. SML of New Jersey requires lots of store and disc space, but it is
25 free and its code sometimes runs faster. Both compilers are perfectly
26 satisfactory for running Isabelle.
28 The Makefiles and make-all use environment variables that you should set
29 according to your site configuration. See file make-all-nj for an example
30 using the Bourne shell, sh.
32 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
33 images. This directory *must* be different from the Isabelle source
34 directory. When using Poly/ML, ISABELLEBIN must be an absolute pathname
35 (one starting with "/").
37 ML_DBASE is an *absolute* pathname to the initial Poly/ML database. It is not
38 required for New Jersey ML.
40 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml". If
41 ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
42 it is Poly/ML; if it begins with the letters "sml" then they assume
43 Standard ML of New Jersey.
45 If a Poly/ML session fails with the message "Run out of store" then you
46 have used up the entire heap. If your tactic is not in a loop, allocating
47 more heap at startup should correct the problem. For instance, "poly -h
48 15000" allocates sufficient heap space to rebuild all Isabelle examples.
51 STRUCTURE OF THIS DIRECTORY
53 The directory Pure containes pure Isabelle, which has no object-logic.
55 Other important files include...
56 COPYRIGHT Copyright notice and Disclaimer of Warranty
57 make-all shell script for building entire system
58 make-all-poly sample make-all invocation for Poly/ML
59 make-all-nj sample make-all invocation for SML of NJ
60 change_simp shell script to help convert sources to new simplifier
61 conv-theory-files.pl perl script to rename old theory files
62 expandshort shell script to expand "shortcuts" in files
63 prove_goal.el Emacs command to change proof format
64 xlisten shell script for running Isabelle under X
65 teeinput shell script to run Isabelle, logging inputs to a file
66 Pure directory of source files for Pure Isabelle
67 Provers directory of generic theorem provers
69 David Aspinall has written a user interface for Isabelle. It runs under
70 GNU Emacs. It's useful to both novices and experts. You can get it by ftp
71 from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
73 A *very* primitive alternative, xlisten sets up a window running Isabelle,
74 with a separate small "listener" window, which keeps a log of all input
75 lines. If you are not running the X Window System, teeinput can still be
76 used to record the log.
78 The following subdirectories contain object-logics:
79 FOL Natural deduction First-Order Logic (intuitionistic and classical)
80 FOLP First-Order Logic with Proof terms
81 ZF Zermelo-Fraenkel set theory
82 HOL Classical Higher-Order Logic
83 LCF Logic for Computable Functions (domain theory) built upon FOL
84 HOLCF A version of LCF built upon HOL
85 CTT Constructive Type Theory
86 LK Classical first-order sequent calculus
87 Modal The modal logics T, S4, S43
88 CCL Martin Coen's Classical Computational Logic
89 Cube Barendregt's Lambda Cube
91 Object-logics include examples files in subdirectory ex or file ex.ML.
92 These files can be loaded in batch mode. The commands can also be
93 executed interactively, using the windows on your workstation. This is a
94 good way to get started.
96 Each object-logic is built on top of Pure Isabelle, and possibly on top of
97 another object logic like FOL or LK. A database or binary called Pure is
98 first created, then the object-logic is loaded on top. Poly/ML extends
99 Pure using its "make_database" operation. Standard ML of New Jersey starts
100 with the Pure core image and loads the object-logic's ROOT.ML.
102 HOW TO GET A STANDARD ML COMPILER
104 To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
105 Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
108 To obtain Standard ML of New Jersey, contact David MacQueen
109 <dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
110 Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to
111 research.att.com; login as anonymous with your userid as password; set
112 binary mode; transfer files from the directory dist/ml.
114 ------------------------------------------------------------------------------
116 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
117 for Isabelle users to discuss problems and exchange information. To join,
118 send a message to isabelle-users-request@cl.cam.ac.uk.
120 ------------------------------------------------------------------------------
122 Please report any problems you encounter. While we shall try to be helpful,
123 we can accept no responsibility for the deficiences of Isabelle and their
126 Lawrence C Paulson E-mail: lcp@cl.cam.ac.uk
127 Computer Laboratory Phone: +44-223-334600
128 University of Cambridge Fax: +44-223-334748
133 Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de
134 Institut für Informatik Phone: +49-89-2105-2690
135 T. U. München Fax: +49-89-2105-8183