author | paulson |
Wed, 27 Nov 1996 10:36:38 +0100 | |
changeset 2237 | f01ac387e82b |
parent 1459 | d12da312eff4 |
child 3511 | da4dd8b7ced4 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: Cube/ROOT |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Tobias Nipkow |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
The Lambda-Cube a la Barendregt |
|
7 |
*) |
|
8 |
||
9 |
val banner = "Barendregt's Lambda-Cube"; |
|
10 |
writeln banner; |
|
11 |
||
393 | 12 |
init_thy_reader(); |
72 | 13 |
|
0 | 14 |
print_depth 1; |
121 | 15 |
use_thy "Cube"; |
0 | 16 |
|
2237 | 17 |
init_pps (); |
0 | 18 |
print_depth 8; |
19 |
||
1459 | 20 |
val Cube_build_completed = (); (*indicate successful build*) |