author | clasohm |
Tue, 16 Nov 1993 14:10:19 +0100 | |
changeset 121 | d392174734e9 |
parent 72 | 099d949fe467 |
child 393 | 02b27671b899 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Cube/ROOT |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
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 |
||
72 | 12 |
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); |
13 |
open Readthy; |
|
14 |
||
0 | 15 |
print_depth 1; |
121 | 16 |
use_thy "Cube"; |
0 | 17 |
|
18 |
use "../Pure/install_pp.ML"; |
|
19 |
print_depth 8; |
|
20 |
||
21 |
val Cube_build_completed = (); (*indicate successful build*) |