isabelle: src/Cube/ROOT.ML@ae31bb7774a7 (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
393 02b27671b899 thy reader now initialised by init_thy_reader(); wenzelm parents: 121 diff changeset	12	init_thy_reader();
72 099d949fe467 changes for new Readthy clasohm parents: 0 diff changeset	13
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	14	print_depth 1;
121 d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 72 diff changeset	15	use_thy "Cube";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	16
a5a9c433f639 Initial revision clasohm parents: diff changeset	17	use "../Pure/install_pp.ML";
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	print_depth 8;
a5a9c433f639 Initial revision clasohm parents: diff changeset	19
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 393 diff changeset	20	make_chart (); (make HTML chart)
ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 393 diff changeset	21
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	22	val Cube_build_completed = (); (indicate successful build)

author	clasohm
	Tue, 24 Oct 1995 14:50:24 +0100
changeset 1296	ae31bb7774a7
parent 393	02b27671b899
child 1361	90d615b599d9
permissions	-rw-r--r--