| author | webertj |
| Sun, 14 Nov 2004 01:40:27 +0100 | |
| changeset 15283 | f21466450330 |
| parent 3279 | 815ef5848324 |
| child 15582 | 7219facb3fd0 |
| permissions | -rw-r--r-- |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY> <H2>LCF: Logic for Computable Functions</H2> This directory contains the ML sources of the Isabelle system for LCF, based on FOL.<p> The <tt>ex</tt> subdirectory contains some examples.<p> Useful references on LCF: <UL> <LI>Lawrence C. Paulson,<BR> Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) </UL> </BODY></HTML>