isabelle: src/Cube/ROOT.ML@a5a9c433f639 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: Cube/ROOT
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Tobias Nipkow
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	The Lambda-Cube a la Barendregt
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	val banner = "Barendregt's Lambda-Cube";
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	writeln banner;
a5a9c433f639 Initial revision clasohm parents: diff changeset	11
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	print_depth 1;
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	use_thy "cube";
a5a9c433f639 Initial revision clasohm parents: diff changeset	14
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	use "../Pure/install_pp.ML";
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	print_depth 8;
a5a9c433f639 Initial revision clasohm parents: diff changeset	17
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	val Cube_build_completed = (); (indicate successful build)

author	clasohm
	Thu, 16 Sep 1993 12:20:38 +0200
changeset 0	a5a9c433f639
child 72	099d949fe467
permissions	-rw-r--r--