Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
(* Title: HOL/MiniML/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TUM
Type inference for let-free MiniML
*)
HOL_build_completed; (*Make examples fail if HOL did*)
writeln"Root file for HOL/MiniML";
Unify.trace_bound := 20;
time_use_thy "I";