src/Cube/ROOT
author wenzelm
Mon Oct 30 20:04:10 2017 +0100 (21 months ago)
changeset 66946 3d8fd98c7c86
parent 51403 2ff3a5589b05
child 69272 15e9ed5b28fb
permissions -rw-r--r--
ROOT cleanup: empty 'document_files' means there is no document;
     1 chapter Cube
     2 
     3 session 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