isabelle: src/HOL/Lambda/ROOT.ML@a9672446b45f (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
11943 a9672446b45f tuned notation; wenzelm parents: 10264 diff changeset	7	Syntax.ambiguity_level := 100;
a9672446b45f tuned notation; wenzelm parents: 10264 diff changeset	8
1269 ee011b365770 New version with eta reduction. nipkow parents: 1165 diff changeset	9	time_use_thy "Eta";
10264 ef384b242d09 use Accessible_Part from HOL/Library; wenzelm parents: 9115 diff changeset	10	time_use_thy "Accessible_Part";
9115 67409447f788 Added new theory. berghofe parents: 9000 diff changeset	11	time_use_thy "Type";