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

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

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

Useful references on Constructive Type Theory: