1chapter Cube
2
3session Cube = Pure +
4  description "
5    Author:     Tobias Nipkow
6    Copyright   1992  University of Cambridge
7
8    Barendregt's Lambda-Cube.
9
10    NB: the formalization is not completely sound!  It does not enforce
11    distinctness of variable names in contexts!
12
13    For more information about the Lambda-Cube, see H. Barendregt, Introduction
14    to Generalised Type Systems, J. Functional Programming.
15  "
16  theories Example
17