isabelle: src/HOL/Lambda/ROOT.ML@4961ecbaaff7 (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
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1126 diff changeset	7	writeln"Root file for HOL/Lambda";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1269 diff changeset	8
1269 ee011b365770 New version with eta reduction. nipkow parents: 1165 diff changeset	9	time_use_thy "Eta";
6490 4961ecbaaff7 improved load paths; wenzelm parents: 6349 diff changeset	10	time_use_thy "../Induct/Acc";
5261 ce3c25c8a694 First steps towards termination of simply typed terms. nipkow parents: 1465 diff changeset	11	time_use_thy "InductTermi";