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: