1
(* Title: Cube/ROOT.ML
2
Author: Tobias Nipkow
3
Copyright 1992 University of Cambridge
4
5
The Lambda-Cube a la Barendregt.
6
*)
7
8
use_thys ["Example"];