src/HOL/Hoare/ROOT.ML
changeset 5646 7c2ddbaf8b8c
parent 1465 5d7a7e439cec
child 6349 f7750d816c21
     1.1 --- a/src/HOL/Hoare/ROOT.ML	Wed Oct 14 11:51:11 1998 +0200
     1.2 +++ b/src/HOL/Hoare/ROOT.ML	Wed Oct 14 15:26:31 1998 +0200
     1.3 @@ -1,10 +1,9 @@
     1.4  (*  Title:      HOL/IMP/ROOT.ML
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7 -    Copyright   1995 TUM
     1.8 +    Copyright   1998 TUM
     1.9  *)
    1.10  
    1.11  HOL_build_completed;    (*Make examples fail if HOL did*)
    1.12  
    1.13  use_thy "Examples";
    1.14 -use_thy "List_Examples";