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)