author | wenzelm |
Fri, 17 Aug 2012 11:23:57 +0200 | |
changeset 48835 | 574042d14fd9 |
parent 48738 | f8c1a5b9488f |
child 51397 | 03b586ee5930 |
permissions | -rw-r--r-- |
session CTT = Pure + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *} options [document = false] theories Main session "CTT-ex" in 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