CTT: Constructive Type Theory

This directory contains the Standard ML sources of the Isabelle system for Constructive Type Theory (extensional equality, no universes). Important files include
ROOT.ML
loads all source files. Enter an ML image containing Pure Isabelle and type: use "ROOT.ML";

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

ex
subdirectory containing examples. To execute them, enter an ML image containing CTT and type: use "ex/ROOT.ML";

Useful references on Constructive Type Theory: