author | wenzelm |
Wed, 03 Feb 1999 17:34:27 +0100 | |
changeset 6216 | 05d99c0bbfa0 |
parent 5261 | ce3c25c8a694 |
child 6349 | f7750d816c21 |
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 |
||
1465 | 7 |
HOL_build_completed; (*Make examples fail if HOL did*) |
1126 | 8 |
|
1165 | 9 |
writeln"Root file for HOL/Lambda"; |
1296 | 10 |
|
1269 | 11 |
time_use_thy "Eta"; |
6216 | 12 |
add_path "../Induct"; |
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
1465
diff
changeset
|
13 |
time_use_thy "InductTermi"; |