author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
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> |