diff -r e74f694ca1da -r c7a8f374339b src/HOL/MiniML/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MiniML/ROOT.ML	Wed Oct 25 09:46:46 1995 +0100
@@ -0,0 +1,17 @@
+(*  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";
+loadpath := [".","MiniML"];
+Unify.trace_bound := 20;
+
+time_use_thy "I";
+
+make_chart ();   (*make HTML chart*)