LCF: Logic for Computable Functions
This directory contains the Standard ML sources of the Isabelle system for
LCF. It is loaded upon FOL, not Pure Isabelle. Important files include
- ROOT.ML
- loads all source files. Enter an ML image containing FOL
Isabelle and type: use "ROOT.ML";
- Makefile
- compiles the files under Poly/ML or SML of New Jersey
- ex.ML
- file containing examples. To execute it, enter an ML image
containing LCF and type: use "ex.ML";
Useful references on First-Order Logic:
- Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)