equal
deleted
inserted
replaced
1 <HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY> |
1 |
|
2 <HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY> |
2 |
3 |
3 <H2>Cube: Barendregt's Lambda-Cube</H2> |
4 <H2>Cube: Barendregt's Lambda-Cube</H2> |
4 |
5 |
5 This directory contains the Standard ML sources of the Isabelle system for |
6 This directory contains the ML sources of the Isabelle system for the |
6 the Lambda-Cube. Important files include |
7 Lambda-Cube.<p> |
7 |
8 |
8 <DL> |
9 The <tt>ex</tt> subdirectory contains some examples.<p> |
9 <DT>ROOT.ML |
|
10 <DD>loads all source files. Enter an ML image containing Pure |
|
11 Isabelle and type: use "ROOT.ML";<P> |
|
12 |
|
13 <DT>Makefile |
|
14 <DD>compiles the files under Poly/ML or SML of New Jersey<P> |
|
15 |
|
16 <DT>ex |
|
17 examples file. To execute them, enter an ML image |
|
18 containing Cube and type: use "ex.ML"; |
|
19 </DL> |
|
20 |
10 |
21 NB: the formalization is not completely sound! It does not enforce |
11 NB: the formalization is not completely sound! It does not enforce |
22 distinctness of variable names in contexts!<P> |
12 distinctness of variable names in contexts!<P> |
23 |
13 |
24 For more information about the Lambda-Cube, see |
14 For more information about the Lambda-Cube, see |
26 <UL> |
16 <UL> |
27 <LI>H. Barendregt<BR> |
17 <LI>H. Barendregt<BR> |
28 Introduction to Generalised Type Systems<BR> |
18 Introduction to Generalised Type Systems<BR> |
29 J. Functional Programming |
19 J. Functional Programming |
30 </UL> |
20 </UL> |
31 </BODY></HTML> |
21 </BODY> |
|
22 </HTML> |