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

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 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$
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	3	Author: Tobias Nipkow
5261 ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: 1465 diff changeset	4	Copyright 1998 TUM
1126 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
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 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";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1269 diff changeset	10
1269 ee011b365770 New version with eta reduction. nipkow parents: 1165 diff changeset	11	time_use_thy "Eta";
5261 ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: 1465 diff changeset	12	loadpath := [".","../Induct"];
ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: 1465 diff changeset	13	time_use_thy "InductTermi";