ISABELLE-93 DISTRIBUTION DIRECTORY ------------------------------------------------------------------------------ ISABELLE-93 IS INCOMPATIBLE WITH EARLIER VERSIONS. PLEASE CONSULT THE DOCUMENTATION. ------------------------------------------------------------------------------ This directory contains the complete Isabelle system. To build and test the entire system, including all object-logics, use the shell script make-all. Pure Isabelle and each of the object-logics can be built separately using the Makefiles in the respective directories; read them for more information. THE MAKEFILES The Makefiles can use two different Standard ML compilers: Poly/ML version 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or later). Poly/ML is a commercial product and costs money, but it is reliable and its database system is convenient for interactive work. SML of New Jersey requires lots of store and disc space, but it is free and its code sometimes runs faster. Both compilers are perfectly satisfactory for running Isabelle. The Makefiles and make-all use environment variables that you should set according to your site configuration. See file make-all-nj for an example using the Bourne shell, sh. ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML images. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one starting with "/"). ML_DBASE is an *absolute* pathname to the initial Poly/ML database (not required for New Jersey ML). ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml". If ISABELLECOMP begins with the letters "poly" then the Makefiles assume that it is Poly/ML; if it begins with the letters "sml" then they assume Standard ML of New Jersey. If a Poly/ML session fails with the message "Run out of store" then you have used up the entire heap. If your tactic is not in a loop, allocating more heap at startup should correct the problem. For instance, "poly -h 15000" allocates sufficient heap space to rebuild all Isabelle examples. STRUCTURE OF THIS DIRECTORY The directory Pure containes pure Isabelle, which has no object-logic. Other important files include... COPYRIGHT Copyright notice and Disclaimer of Warranty make-all shell script for building entire system make-all-poly sample make-all invocation for Poly/ML make-all-nj sample make-all invocation for SML of NJ change_simp shell script to help convert sources to new simplifier expandshort shell script to expand "shortcuts" in files prove_goal.el Emacs command to change proof format xlisten shell script for running Isabelle under X teeinput shell script to run Isabelle, logging inputs to a file Pure directory of source files for Pure Isabelle Provers directory of generic theorem provers xlisten sets up a window running Isabelle, with a separate small "listener" window, which keeps a log of all input lines. This log is a useful record of a session. If you are not running X windows, teeinput can still be used at least to record (if not to display) the log. The following subdirectories contain object-logics: FOL Natural deduction First-Order Logic (intuitionistic and classical) FOLP First-Order Logic with Proof terms ZF Zermelo-Fraenkel set theory HOL Classical Higher-Order Logic LCF Logic for Computable Functions (domain theory) built upon FOL HOLCF A version of LCF built upon HOL CTT Constructive Type Theory LK Classical first-order sequent calculus Modal The modal logics T, S4, S43 CCL Martin Coen's Classical Computational Logic Cube Barendregt's Lambda Cube Object-logics include examples files in subdirectory ex or file ex.ML. These files can be loaded in batch mode. The commands can also be executed interactively, using the windows on your workstation. This is a good way to get started. Each object-logic is built on top of Pure Isabelle, and possibly on top of another object logic like FOL or LK. A database or binary called Pure is first created, then the object-logic is loaded on top. Poly/ML extends Pure using its "make_database" operation. Standard ML of New Jersey starts with the Pure core image and loads the object-logic's ROOT.ML. HOW TO GET A STANDARD ML COMPILER To obtain Poly/ML, contact Mike Crawley at Abstract Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH, England. To obtain Standard ML of New Jersey, contact David MacQueen at AT&T Bell Laboratories, 600 Mountain Avenue, Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to research.att.com; login as anonymous with your userid as password; set binary mode; transfer files from the directory dist/ml. ------------------------------------------------------------------------------ The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems and exchange information. To join, send a message to isabelle-users-request@cl.cam.ac.uk. ------------------------------------------------------------------------------ Please report any problems you encounter. While we shall try to be helpful, we can accept no responsibility for the deficiences of Isabelle and their consequences. Lawrence C Paulson E-mail: lcp@cl.cam.ac.uk Computer Laboratory Phone: +44-223-334600 University of Cambridge Fax: +44-223-334748 Pembroke Street Cambridge CB2 3QG England Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de Institut fuer Informatik Phone: +49-89-2105-2690 T. U. Muenchen Fax: +49-89-2105-8183 D-80290 Muenchen Germany Last updated 13 May 1994