author | wenzelm |
Tue, 29 Sep 2015 18:39:55 +0200 | |
changeset 61281 | 11c1bf92d61d |
parent 51403 | 2ff3a5589b05 |
child 66946 | 3d8fd98c7c86 |
permissions | -rw-r--r-- |
chapter Cube session Cube = Pure + description {* Author: Tobias Nipkow Copyright 1992 University of Cambridge 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