author | wenzelm |
Fri, 11 Jan 2013 22:23:03 +0100 | |
changeset 50838 | ad959a8b951e |
parent 48738 | f8c1a5b9488f |
child 51397 | 03b586ee5930 |
permissions | -rw-r--r-- |
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
1 |
session CTT = Pure + |
48475 | 2 |
description {* |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
6 |
options [document = false] |
48475 | 7 |
theories Main |
8 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
9 |
session "CTT-ex" in ex = CTT + |
48475 | 10 |
description {* |
11 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
12 |
Copyright 1991 University of Cambridge |
|
13 |
||
14 |
Examples for Constructive Type Theory. |
|
15 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
16 |
options [document = false] |
48475 | 17 |
theories Typechecking Elimination Equality Synthesis |