author | wenzelm |
Wed, 06 Mar 2002 17:48:39 +0100 | |
changeset 13031 | 3f7824dd8ddf |
parent 11943 | a9672446b45f |
child 13550 | 5a176b8dda84 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Lambda/ROOT.ML |
1126 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
1465
diff
changeset
|
4 |
Copyright 1998 TUM |
1126 | 5 |
*) |
6 |
||
11943 | 7 |
Syntax.ambiguity_level := 100; |
8 |
||
1269 | 9 |
time_use_thy "Eta"; |
13031 | 10 |
no_document time_use_thy "Accessible_Part"; |
9115 | 11 |
time_use_thy "Type"; |