| author | wenzelm | 
| Thu, 20 Sep 2012 21:31:56 +0200 | |
| changeset 49473 | ca7e2c21b104 | 
| 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  |