1
(* Title: HOL/MiniML/ROOT.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1995 TUM
5
6
Type inference for let-free MiniML
7
*)
8
9
HOL_build_completed; (*Make examples fail if HOL did*)
10
11
writeln"Root file for HOL/MiniML";
12
Unify.trace_bound := 20;
13
14
time_use_thy "I";