src/Cube/README.html
author wenzelm
Tue, 06 May 1997 15:27:35 +0200
changeset 3118 24dae6222579
parent 1341 69fec018854c
child 3279 815ef5848324
permissions -rw-r--r--
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);

<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>

<H2>Cube: Barendregt's Lambda-Cube</H2>

This directory contains the Standard ML sources of the Isabelle system for
the Lambda-Cube.  Important files include

<DL>
<DT>ROOT.ML
<DD>loads all source files.  Enter an ML image containing Pure
Isabelle and type: use "ROOT.ML";<P>

<DT>Makefile
<DD>compiles the files under Poly/ML or SML of New Jersey<P>

<DT>ex
examples file. To execute them, enter an ML image
containing Cube and type: use "ex.ML";
</DL>

NB: the formalization is not completely sound!  It does not enforce
distinctness of variable names in contexts!<P>

For more information about the Lambda-Cube, see

<UL>
<LI>H. Barendregt<BR>
    Introduction to Generalised Type Systems<BR>
    J. Functional Programming
</UL>
</BODY></HTML>