equal
deleted
inserted
replaced
1 <HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY> |
1 <HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY> |
2 |
2 |
3 <H2>LCF: Logic for Computable Functions</H2> |
3 <H2>LCF: Logic for Computable Functions</H2> |
4 |
4 |
5 This directory contains the Standard ML sources of the Isabelle system for |
5 This directory contains the ML sources of the Isabelle system for |
6 LCF. It is loaded upon FOL, not Pure Isabelle. Important files include |
6 LCF, based on FOL.<p> |
7 |
7 |
8 <DL> |
8 The <tt>ex</tt> subdirectory contains some examples.<p> |
9 <DT>ROOT.ML |
|
10 <DD>loads all source files. Enter an ML image containing FOL |
|
11 Isabelle and type: use "ROOT.ML";<P> |
|
12 |
9 |
13 <DT>Makefile |
10 Useful references on LCF: |
14 <DD>compiles the files under Poly/ML or SML of New Jersey<P> |
|
15 |
|
16 <DT>ex.ML |
|
17 <DD>file containing examples. To execute it, enter an ML image |
|
18 containing LCF and type: use "ex.ML"; |
|
19 </DL> |
|
20 |
|
21 Useful references on First-Order Logic: |
|
22 |
11 |
23 <UL> |
12 <UL> |
24 <LI>Lawrence C. Paulson,<BR> |
13 <LI>Lawrence C. Paulson,<BR> |
25 Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) |
14 Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) |
26 </UL> |
15 </UL> |