(* Title: Cube/ROOT.ML ID: $Id: ROOT.ML,v 1.14 2005/09/17 10:50:57 wenzelm Exp $ Author: Tobias Nipkow Copyright 1992 University of Cambridge The Lambda-Cube a la Barendregt. *) val banner = "Barendregt's Lambda-Cube"; writeln banner; use_thy "Cube"; use_thy "Example";