author | wenzelm |
Fri, 07 Mar 1997 11:48:46 +0100 | |
changeset 2754 | 59bd96046ad6 |
parent 2525 | 477c05586286 |
child 6349 | f7750d816c21 |
permissions | -rw-r--r-- |
2031 | 1 |
(* Title: HOL/MiniML/ROOT.ML |
1300 | 2 |
ID: $Id$ |
2525 | 3 |
Author: Wolfgang Naraschewski and Tobias Nipkow |
1300 | 4 |
Copyright 1995 TUM |
5 |
||
2525 | 6 |
Type inference for MiniML |
1300 | 7 |
*) |
8 |
||
2031 | 9 |
HOL_build_completed; (*Make examples fail if HOL did*) |
1300 | 10 |
|
11 |
writeln"Root file for HOL/MiniML"; |
|
12 |
||
2525 | 13 |
time_use_thy "W"; |