| author | wenzelm | 
| Sun, 24 Aug 2025 20:26:02 +0200 | |
| changeset 83053 | c1ccd17fb70f | 
| parent 75992 | 1f6d79b62222 | 
| permissions | -rw-r--r-- | 
| 75992 | 1 | chapter Misc | 
| 51397 
03b586ee5930
support for 'chapter' specifications within session ROOT;
 wenzelm parents: 
48738diff
changeset | 2 | |
| 48738 
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
 wenzelm parents: 
48483diff
changeset | 3 | session Cube = Pure + | 
| 69319 | 4 | description " | 
| 48475 | 5 | Author: Tobias Nipkow | 
| 6 | Copyright 1992 University of Cambridge | |
| 7 | ||
| 51403 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 8 | Barendregt's Lambda-Cube. | 
| 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 9 | |
| 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 10 | NB: the formalization is not completely sound! It does not enforce | 
| 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 11 | distinctness of variable names in contexts! | 
| 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 12 | |
| 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 13 | For more information about the Lambda-Cube, see H. Barendregt, Introduction | 
| 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
 wenzelm parents: 
51397diff
changeset | 14 | to Generalised Type Systems, J. Functional Programming. | 
| 69319 | 15 | " | 
| 48475 | 16 | theories Example |