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

3511 da4dd8b7ced4 removed obsolete init_pps and init_thy_reader; wenzelm parents: 2237 diff changeset	1	(* Title: Cube/ROOT.ML
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1459 d12da312eff4 expanded tabs clasohm parents: 1361 diff changeset	3	Author: Tobias Nipkow
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
3511 da4dd8b7ced4 removed obsolete init_pps and init_thy_reader; wenzelm parents: 2237 diff changeset	6	The Lambda-Cube a la Barendregt.
0 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
3941 ea440c63d206 qualified names; wenzelm parents: 3511 diff changeset	12	reset global_names;
ea440c63d206 qualified names; wenzelm parents: 3511 diff changeset	13
3511 da4dd8b7ced4 removed obsolete init_pps and init_thy_reader; wenzelm parents: 2237 diff changeset	14	print_depth 1;
72 099d949fe467 changes for new Readthy clasohm parents: 0 diff changeset	15
121 d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 72 diff changeset	16	use_thy "Cube";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	17
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	print_depth 8;
a5a9c433f639 Initial revision clasohm parents: diff changeset	19
1459 d12da312eff4 expanded tabs clasohm parents: 1361 diff changeset	20	val Cube_build_completed = (); (indicate successful build)

author	wenzelm
	Mon, 20 Oct 1997 11:01:07 +0200
changeset 3941	ea440c63d206
parent 3511	da4dd8b7ced4
child 4024	3c056eab237c
permissions	-rw-r--r--