author | paulson |
Mon, 07 Oct 1996 10:34:58 +0200 | |
changeset 2058 | ff04984186e9 |
parent 2031 | 03a843f0f447 |
child 2525 | 477c05586286 |
permissions | -rw-r--r-- |
2031 | 1 |
(* Title: HOL/MiniML/ROOT.ML |
1300 | 2 |
ID: $Id$ |
2031 | 3 |
Author: Tobias Nipkow |
1300 | 4 |
Copyright 1995 TUM |
5 |
||
6 |
Type inference for let-free MiniML |
|
7 |
*) |
|
8 |
||
2031 | 9 |
HOL_build_completed; (*Make examples fail if HOL did*) |
1300 | 10 |
|
11 |
writeln"Root file for HOL/MiniML"; |
|
12 |
Unify.trace_bound := 20; |
|
13 |
||
1925 | 14 |
AddSEs [less_SucE]; |
15 |
||
1300 | 16 |
time_use_thy "I"; |