# HG changeset patch # User wenzelm # Date 866799473 -7200 # Node ID 40b1287347d77f58497325fd20b6e27f87f1a719 # Parent b2ecba22b8be7acce3ab7dd02172846ee3c5e037 removed; diff -r b2ecba22b8be -r 40b1287347d7 NEWS --- a/NEWS Fri Jun 20 11:34:05 1997 +0200 +++ b/NEWS Fri Jun 20 11:37:53 1997 +0200 @@ -2,6 +2,12 @@ Isabelle NEWS -- history of user-visible changes ================================================ +New in Isabelle???? (DATE ????) +------------------------------- + +* removed old README and Makefiles; + + New in Isabelle94-8 (May 1997) ------------------------------ diff -r b2ecba22b8be -r 40b1287347d7 README.old --- a/README.old Fri Jun 20 11:34:05 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,164 +0,0 @@ - -*************************************************************************** - -IMPORTANT NOTE: This is the old README. The installation procedure -described below basically still works for Isabelle94-8, but will be -phased out next time. - -*************************************************************************** - - - - ISABELLE-94 DISTRIBUTION DIRECTORY - ------------------------------------------------------------------------------- -ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS. PLEASE CONSULT THE -DOCUMENTATION. - -In particular, theory files are no longer forced into lower case, but must -be identical to the actual theory name. See the script -conv-theory-files.pl on directory Tools. ------------------------------------------------------------------------------- - -This directory contains the complete Isabelle system. To build and test -all the Isabelle object-logics, use the shell script make-all (on directory -Tools). Pure Isabelle and each of the object-logics can be built -separately using the Makefiles in the respective directories; read them for -more information. - - HOW TO BUILD ISABELLE - -Here are brief instructions. For more detail, read further. - -1. Create a directory to hold the Isabelle executable images. - Set the environment variable ISABELLEBIN to its full (absolute) pathname. - -2. Set the environment variable ISABELLECOMP to the command to execute your - Standard ML compiler. - -3. If using Poly/ML, set the environment variable ML_DBASE to the full - pathname of the empty Poly/ML database. - -4. Change your working directory to that containing this file. - -5a. To build ALL logics and run examples, type "make-all" and wait up to - 10 hours. Standard ML of New Jersey will require up to 200M - of disc space! Poly/ML will require about 25M. - --OR- -5b. To build ALL logics but run no examples, type "make-all -notest". This - is much faster than 5a but needs just as much disc space. - --OR- -5c. To build just one logic, such as HOL, change to directory HOL and type - "make" or "make test". This may trigger further Makes automatically. - - - SUITABLE ML COMPILERS - -You 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 stable and -efficient; moreover its database system is convenient for interactive work. -SML/NJ needs lots of store and disc space, but it is free. Some recent -versions of SML/NJ are significantly faster than 0.93, but beware of many -incompatibilities among them; you might be forced to edit the file -Pure/NJ1xx.ML. VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW. - -To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel -University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk. - -To obtain Standard ML of New Jersey, see the Web page - http://cm.bell-labs.com/cm/cs/what/smlnj/software.html -or send email to sml-nj@research.bell-labs.com. - - - ENVIRONMENT VARIABLES - -The Makefiles and make-all use environment variables that you should set -according to your site configuration. See file Tools/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. This directory *must* be different from the Isabelle source -directory. ISABELLEBIN must be an absolute pathname (one starting with "/"). - -ML_DBASE is an *absolute* pathname to the initial Poly/ML database. It is not -required for New Jersey ML. - -ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly --noDisplay -h 15000". (The -h switch to Poly specifies an initial heap -allocation, which you should consider increasing if a command fails with the -message "Run out of store".) Please DO NOT use a command such as -"sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the -Makefiles. - -If, after stripping a leading pathname, the compiler begins with the letters -"poly" then the Makefiles assume Poly/ML. If it begins with the letters "sml" -then they assume Standard ML of New Jersey. - - - STRUCTURE OF THIS DIRECTORY - -Important files include... - COPYRIGHT Copyright notice and Disclaimer of Warranty - Pure contains source files for Pure Isabelle (no object-logic) - Provers contains generic theorem provers: simplifier, etc. - Tools contains shell scripts and utilities - -The following subdirectories contain object-logics: - FOL natural deduction First-Order Logic - (intuitionistic and classical versions) - 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 - Sequents Sequent calcul: first-order logic - modal logics T, S4, S43 - intuitionistic linear logic - CCL Martin Coen's Classical Computational Logic - Cube Barendregt's Lambda Cube - -David Aspinall has written a user interface for Isabelle. It runs under -GNU Emacs. It's useful to both novices and experts. You can get it by ftp -from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz. - -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 HOL. 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. - ------------------------------------------------------------------------------- - -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 für Informatik Phone: +49-89-2105-2690 -T. U. München Fax: +49-89-2105-8183 -D-80290 München -Germany - -$Id$