File: README.NJ -- the readme file accompanying the distribution of ISABELLE-90 from research.att.com and princeton.edu The file isabelle.tar.Z found in this directory is a compressed tarred directory containing the files necessary to build the theorem proving system ISABELLE-90 by Lawrence C. Paulson of the University of Cambridge, Cambridge, England. This version of ISABELLE-90 is suitable for building under Standard ML of New Jersey (SML/NJ), version 0.56, which may also be obtained from this directory. There are a few changes that have been made to the code that reflect changes in SML/NJ version 0.56 over version 0.44. The changes made are in the files src/NEWROOT.ML and src/PolyML.ML. The code that has been replaced is commented as (* for Version 0.44 *), to make it readily possible to reconvert the code to run under SML/NJ version 0.44. To extract the files contained in isabelle.tar.Z, you should execute the following commands: mkdir isa mv isabelle.tar.Z isa cd isa uncompress -c isabelle.tar.Z | tar xf - Once you have completed those commands, the directory should contain the files announce, License, and README.NJ (a copy of this file), and it should contain the directory src/ which contains the .ML files for building Isabelle. To build the executable code for the base system of ISABELLE-90 in SML/NJ, assuming that SML/NJ version 0.56 is invoked in your system by the command sml, you should change directories into src/ and execute the following: echo 'use "NEWROOT.ML"' | sml > isa.LOG & This will create an executable file named EXEC, and output a log of the building into the file isa.LOG. In case you have difficulties, there is a sample log in the file sample.LOG. If you wish to build any of the object logics that come with ISABELLE-90, you will first need to place the file make-rulenames in a directory on the search path for shell commands, to permit its execution on any subdirectory. Each object language directory has a file named ROOT.ML that may be loaded in EXEC (with the "use" function) to build the corresponding object language, and a file ex/ROOT.ML that executes a few examples when loaded. See src/README for further details. A TeX version of a manual for isabelle is found in the directory DOC/. Questions about ISABELLE-90 should be directed to Lawrence C. Paulson, ADDRESS UNTIL JULY 1990 Lawrence C Paulson E-mail: lcp@lfcs.ed.ac.uk Department of Computer Science Phone: +44-31-667-1081 University of Edinburgh Mayfield Road Edinburgh EH9 3JZ Scotland NORMAL ADDRESS 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