removed;
authorwenzelm
Fri Jun 20 11:37:53 1997 +0200 (1997-06-20)
changeset 345440b1287347d7
parent 3453 b2ecba22b8be
child 3455 fbd4eb0cd0da
removed;
NEWS
README.old
     1.1 --- a/NEWS	Fri Jun 20 11:34:05 1997 +0200
     1.2 +++ b/NEWS	Fri Jun 20 11:37:53 1997 +0200
     1.3 @@ -2,6 +2,12 @@
     1.4  Isabelle NEWS -- history of user-visible changes
     1.5  ================================================
     1.6  
     1.7 +New in Isabelle???? (DATE ????)
     1.8 +-------------------------------
     1.9 +
    1.10 +* removed old README and Makefiles;
    1.11 +
    1.12 +
    1.13  New in Isabelle94-8 (May 1997)
    1.14  ------------------------------
    1.15  
     2.1 --- a/README.old	Fri Jun 20 11:34:05 1997 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,164 +0,0 @@
     2.4 -
     2.5 -***************************************************************************
     2.6 -
     2.7 -IMPORTANT NOTE: This is the old README. The installation procedure
     2.8 -described below basically still works for Isabelle94-8, but will be
     2.9 -phased out next time.
    2.10 -
    2.11 -***************************************************************************
    2.12 -
    2.13 -
    2.14 -
    2.15 -		     ISABELLE-94 DISTRIBUTION DIRECTORY
    2.16 -
    2.17 -------------------------------------------------------------------------------
    2.18 -ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
    2.19 -DOCUMENTATION.  
    2.20 -
    2.21 -In particular, theory files are no longer forced into lower case, but must
    2.22 -be identical to the actual theory name.  See the script
    2.23 -conv-theory-files.pl on directory Tools.
    2.24 -------------------------------------------------------------------------------
    2.25 -
    2.26 -This directory contains the complete Isabelle system.  To build and test
    2.27 -all the Isabelle object-logics, use the shell script make-all (on directory
    2.28 -Tools).  Pure Isabelle and each of the object-logics can be built
    2.29 -separately using the Makefiles in the respective directories; read them for
    2.30 -more information.
    2.31 -
    2.32 -			HOW TO BUILD ISABELLE
    2.33 -
    2.34 -Here are brief instructions.  For more detail, read further.
    2.35 -
    2.36 -1.  Create a directory to hold the Isabelle executable images.
    2.37 -    Set the environment variable ISABELLEBIN to its full (absolute) pathname.
    2.38 -
    2.39 -2.  Set the environment variable ISABELLECOMP to the command to execute your
    2.40 -    Standard ML compiler.
    2.41 -
    2.42 -3.  If using Poly/ML, set the environment variable ML_DBASE to the full 
    2.43 -    pathname of the empty Poly/ML database.
    2.44 -
    2.45 -4.  Change your working directory to that containing this file.
    2.46 -
    2.47 -5a. To build ALL logics and run examples, type "make-all" and wait up to 
    2.48 -    10 hours.  Standard ML of New Jersey will require up to 200M
    2.49 -    of disc space!  Poly/ML will require about 25M.
    2.50 -
    2.51 --OR-
    2.52 -5b. To build ALL logics but run no examples, type "make-all -notest".  This
    2.53 -    is much faster than 5a but needs just as much disc space.
    2.54 -
    2.55 --OR-
    2.56 -5c. To build just one logic, such as HOL, change to directory HOL and type
    2.57 -    "make" or "make test".  This may trigger further Makes automatically.
    2.58 -
    2.59 -
    2.60 -			SUITABLE ML COMPILERS
    2.61 -
    2.62 -You can use two different Standard ML compilers: Poly/ML version 2.03 or later
    2.63 -(from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
    2.64 -later).  Poly/ML is a commercial product and costs money, but it is stable and
    2.65 -efficient; moreover its database system is convenient for interactive work.
    2.66 -SML/NJ needs lots of store and disc space, but it is free.  Some recent
    2.67 -versions of SML/NJ are significantly faster than 0.93, but beware of many
    2.68 -incompatibilities among them; you might be forced to edit the file
    2.69 -Pure/NJ1xx.ML.  VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW.
    2.70 -
    2.71 -To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
    2.72 -University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk.
    2.73 -
    2.74 -To obtain Standard ML of New Jersey, see the Web page 
    2.75 -	http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
    2.76 -or send email to sml-nj@research.bell-labs.com.
    2.77 -
    2.78 -
    2.79 -			ENVIRONMENT VARIABLES
    2.80 -
    2.81 -The Makefiles and make-all use environment variables that you should set
    2.82 -according to your site configuration.  See file Tools/make-all-nj for an
    2.83 -example using the Bourne shell, sh.
    2.84 -
    2.85 -ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    2.86 -images.  This directory *must* be different from the Isabelle source
    2.87 -directory.  ISABELLEBIN must be an absolute pathname (one starting with "/").
    2.88 -
    2.89 -ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    2.90 -required for New Jersey ML.
    2.91 -
    2.92 -ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
    2.93 --noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
    2.94 -allocation, which you should consider increasing if a command fails with the
    2.95 -message "Run out of store".)  Please DO NOT use a command such as
    2.96 -"sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the
    2.97 -Makefiles. 
    2.98 -
    2.99 -If, after stripping a leading pathname, the compiler begins with the letters
   2.100 -"poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
   2.101 -then they assume Standard ML of New Jersey.
   2.102 -
   2.103 -
   2.104 -			 STRUCTURE OF THIS DIRECTORY
   2.105 -
   2.106 -Important files include...
   2.107 -  COPYRIGHT 	Copyright notice and Disclaimer of Warranty
   2.108 -  Pure		contains source files for Pure Isabelle (no object-logic)
   2.109 -  Provers	contains generic theorem provers: simplifier, etc.
   2.110 -  Tools		contains shell scripts and utilities 
   2.111 -
   2.112 -The following subdirectories contain object-logics:
   2.113 -  FOL 		natural deduction First-Order Logic 
   2.114 -			(intuitionistic and classical versions)
   2.115 -  FOLP 		First-Order Logic with Proof terms
   2.116 -  ZF		Zermelo-Fraenkel set theory
   2.117 -  HOL		Classical Higher-Order Logic
   2.118 -  LCF		Logic for Computable Functions (domain theory) built upon FOL
   2.119 -  HOLCF		A version of LCF built upon HOL
   2.120 -  CTT		Constructive Type Theory
   2.121 -  Sequents	Sequent calcul: first-order logic
   2.122 -				modal logics T, S4, S43
   2.123 -				intuitionistic linear logic
   2.124 -  CCL		Martin Coen's Classical Computational Logic
   2.125 -  Cube		Barendregt's Lambda Cube
   2.126 -
   2.127 -David Aspinall has written a user interface for Isabelle.  It runs under
   2.128 -GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
   2.129 -from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
   2.130 -
   2.131 -Object-logics include examples files in subdirectory ex or file ex.ML.
   2.132 -These files can be loaded in batch mode.  The commands can also be
   2.133 -executed interactively, using the windows on your workstation.  This is a
   2.134 -good way to get started.
   2.135 -
   2.136 -Each object-logic is built on top of Pure Isabelle, and possibly on top of
   2.137 -another object logic like FOL or HOL.  A database or binary called Pure is
   2.138 -first created, then the object-logic is loaded on top.  Poly/ML extends
   2.139 -Pure using its "make_database" operation.  Standard ML of New Jersey starts
   2.140 -with the Pure core image and loads the object-logic's ROOT.ML.
   2.141 -
   2.142 -------------------------------------------------------------------------------
   2.143 -
   2.144 -The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
   2.145 -for Isabelle users to discuss problems and exchange information.  To join,
   2.146 -send a message to isabelle-users-request@cl.cam.ac.uk.
   2.147 -
   2.148 -------------------------------------------------------------------------------
   2.149 -
   2.150 -Please report any problems you encounter.  While we shall try to be helpful,
   2.151 -we can accept no responsibility for the deficiences of Isabelle and their
   2.152 -consequences.
   2.153 -
   2.154 -Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
   2.155 -Computer Laboratory 		Phone: +44-223-334600
   2.156 -University of Cambridge 	Fax:   +44-223-334748 
   2.157 -Pembroke Street 
   2.158 -Cambridge CB2 3QG 
   2.159 -England
   2.160 -
   2.161 -Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   2.162 -Institut für Informatik		Phone: +49-89-2105-2690
   2.163 -T. U. München			Fax:   +49-89-2105-8183
   2.164 -D-80290 München
   2.165 -Germany
   2.166 -
   2.167 -$Id$