| author | wenzelm |
| Tue, 24 Jul 2012 21:26:28 +0200 | |
| changeset 48486 | 691d0b44a793 |
| parent 48483 | 9bfb6978eb80 |
| child 48738 | f8c1a5b9488f |
| permissions | -rw-r--r-- |
session CTT! in "." = Pure + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *} options [document = false] theories Main session ex = CTT + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Examples for Constructive Type Theory. *} options [document = false] theories Typechecking Elimination Equality Synthesis