(* Title: Cube/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge The Lambda-Cube a la Barendregt. *) use_thys ["Cube", "Example"];