| author | berghofe |
| Fri, 15 Oct 1999 12:31:43 +0200 | |
| changeset 7871 | 30fb773113a1 |
| parent 3279 | 815ef5848324 |
| child 15283 | f21466450330 |
| permissions | -rw-r--r-- |
| 3279 | 1 |
<HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY> |
| 1341 | 2 |
|
3 |
<H2>LCF: Logic for Computable Functions</H2> |
|
4 |
||
| 3279 | 5 |
This directory contains the ML sources of the Isabelle system for |
6 |
LCF, based on FOL.<p> |
|
| 1341 | 7 |
|
| 3279 | 8 |
The <tt>ex</tt> subdirectory contains some examples.<p> |
| 1341 | 9 |
|
| 3279 | 10 |
Useful references on LCF: |
| 1341 | 11 |
|
12 |
<UL> |
|
13 |
<LI>Lawrence C. Paulson,<BR> |
|
14 |
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) |
|
15 |
</UL> |
|
16 |
</BODY></HTML> |