author | clasohm |
Fri, 22 Oct 1993 13:35:15 +0100 | |
changeset 72 | 099d949fe467 |
parent 0 | a5a9c433f639 |
child 121 | d392174734e9 |
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; structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); open Readthy; print_depth 1; use_thy "cube"; use "../Pure/install_pp.ML"; print_depth 8; val Cube_build_completed = (); (*indicate successful build*)