README

removal of obsolete type-declaration syntax

+
−		     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 enviroment variables that you should set
+
−according to your site configuration.
+
−
+
−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
+
−  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
+
−  CTT	  Constructive Type Theory
+
−  HOL	  Classical Higher-Order Logic
+
−  LK	  Classical first-order sequent calculus
+
−  Modal	  The modal logics T, S4, S43
+
−  LCF     Logic for Computable Functions (domain theory)
+
−  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 <[e-mail]> at Abstract
+
−Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
+
−England.
+
−
+
−To obtain Standard ML of New Jersey, contact David MacQueen
+
−<[e-mail]> 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 [e-mail] provides a forum
+
−for Isabelle users to discuss problems and exchange information.  To join,
+
−send a message to [e-mail].
+
−
+
−------------------------------------------------------------------------------
+
−
+
−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: [e-mail]
+
−Computer Laboratory 		Phone: [phone]
+
−University of Cambridge 	Fax:   [phone] 
+
−Pembroke Street 
+
−Cambridge CB2 3QG 
+
−England
+
−
+
−Tobias Nipkow			E-mail: [e-mail]
+
−Institut fuer Informatik	Phone: [phone]
+
−T. U. Muenchen			Fax:   [phone]
+
−D-80290 Muenchen
+
−Germany
+
−
+
−Last updated 13 December 1993