Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
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 and
type: use "ROOT.ML";
Makefile -- compiles the files under Poly/ML or SML of New Jersey
ex.ML -- files containing examples. To execute them, enter an ML image
containing LCF and type: use "ex.ML";
Useful references on LCF:
Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)