isabelle: src/HOL/Lambda/ROOT.ML@89550840ef93 (annotated)

1269 ee011b365770 New version with eta reduction. nipkow parents: 1165 diff changeset	1	(* Title: HOL/Lambda/ROOT.ML
1126 50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	2	ID: $Id$
50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	3	Author: Tobias Nipkow
50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	4	Copyright 1995 TUM
50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	5	*)
50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	6
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1126 diff changeset	7	HOL_build_completed; (Make examples fail if HOL did)
1126 50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	8
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1126 diff changeset	9	writeln"Root file for HOL/Lambda";
1126 50ac36140e21 Moved comment from ParRed.thy to ROOT.ML nipkow parents: diff changeset	10	loadpath := [".","Lambda"];
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1269 diff changeset	11
1269 ee011b365770 New version with eta reduction. nipkow parents: 1165 diff changeset	12	time_use_thy "Eta";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1269 diff changeset	13
ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1269 diff changeset	14	make_chart (); (make HTML chart)

author	nipkow
	Sun, 19 Nov 1995 14:17:31 +0100
changeset 1347	89550840ef93
parent 1296	ae31bb7774a7
child 1351	4a960c012383
permissions	-rw-r--r--