src/HOL/Hoare/ROOT.ML

--- a/src/HOL/Hoare/ROOT.ML	Wed Oct 14 11:51:11 1998 +0200
+++ b/src/HOL/Hoare/ROOT.ML	Wed Oct 14 15:26:31 1998 +0200
@@ -1,10 +1,9 @@
 (*  Title:      HOL/IMP/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1995 TUM
+    Copyright   1998 TUM
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 use_thy "Examples";
-use_thy "List_Examples";