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