## LCF: Logic for Computable Functions

This directory contains the ML sources of the Isabelle system for
LCF, based on FOL.
The `ex` subdirectory contains some examples.

Useful references on LCF:

- Lawrence C. Paulson,

Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)