equal
deleted
inserted
replaced
1 session CTT! in "." = Pure + |
1 session CTT = Pure + |
2 description {* |
2 description {* |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 *} |
5 *} |
6 options [document = false] |
6 options [document = false] |
7 theories Main |
7 theories Main |
8 |
8 |
9 session ex = CTT + |
9 session "CTT-ex" in ex = CTT + |
10 description {* |
10 description {* |
11 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
11 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
12 Copyright 1991 University of Cambridge |
12 Copyright 1991 University of Cambridge |
13 |
13 |
14 Examples for Constructive Type Theory. |
14 Examples for Constructive Type Theory. |