| changeset 48475 | 02dd825f5a4e |
| child 48483 | 9bfb6978eb80 |
| 48474:5b9d79c6323b | 48475:02dd825f5a4e |
|---|---|
1 session CTT! in "." = Pure + |
|
2 description {* |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 *} |
|
6 theories Main |
|
7 |
|
8 session ex = CTT + |
|
9 description {* |
|
10 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
11 Copyright 1991 University of Cambridge |
|
12 |
|
13 Examples for Constructive Type Theory. |
|
14 *} |
|
15 theories Typechecking Elimination Equality Synthesis |