author | clasohm |
Tue, 21 Nov 1995 15:10:12 +0100 | |
changeset 1361 | 90d615b599d9 |
parent 1296 | ae31bb7774a7 |
child 1459 | d12da312eff4 |
permissions | -rw-r--r-- |
(* Title: Cube/ROOT ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge The Lambda-Cube a la Barendregt *) val banner = "Barendregt's Lambda-Cube"; writeln banner; init_thy_reader(); print_depth 1; use_thy "Cube"; use "../Pure/install_pp.ML"; print_depth 8; val Cube_build_completed = (); (*indicate successful build*)