src/HOL/Hoare/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/ROOT.ML	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,12 @@
+(*  Title: 	HOL/IMP/ROOT.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1995 TUM
+*)
+
+HOL_build_completed;	(*Make examples fail if HOL did*)
+
+loadpath := ["Hoare"];
+use_thy "Examples";
+
+make_chart ();   (*make HTML chart*)