author | wenzelm |
Thu, 08 Nov 2018 22:29:09 +0100 | |
changeset 69272 | 15e9ed5b28fb |
parent 66946 | 3d8fd98c7c86 |
child 69319 | baccaf89ca0d |
permissions | -rw-r--r-- |
chapter Cube session Cube = Pure + description \<open> 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. \<close> theories Example