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
loads all source files. Enter an ML image containing FOL Isabelle and type: use "ROOT.ML";

compiles the files under Poly/ML or SML of New Jersey

file containing examples. To execute it, enter an ML image containing LCF and type: use "ex.ML";
Useful references on First-Order Logic: