--- a/src/Cube/ROOT Tue Mar 12 20:03:04 2013 +0100
+++ b/src/Cube/ROOT Tue Mar 12 21:59:48 2013 +0100
@@ -5,7 +5,13 @@
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
- The Lambda-Cube a la Barendregt.
+ Barendregt's Lambda-Cube.
+
+ NB: the formalization is not completely sound! It does not enforce
+ distinctness of variable names in contexts!
+
+ For more information about the Lambda-Cube, see H. Barendregt, Introduction
+ to Generalised Type Systems, J. Functional Programming.
*}
options [document = false]
theories Example