src/HOL/Hoare/ROOT.ML
changeset 14028 ff6eb32b30a1
parent 13875 12997e3ddd8d
child 24104 719fbe4fb77f
     1.1 --- a/src/HOL/Hoare/ROOT.ML	Wed May 14 11:15:18 2003 +0200
     1.2 +++ b/src/HOL/Hoare/ROOT.ML	Wed May 14 14:20:55 2003 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/IMP/ROOT.ML
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7 -    Copyright   1998 TUM
     1.8 +    Copyright   1998-2003 TUM
     1.9  *)
    1.10  
    1.11  time_use_thy "Examples";
    1.12 @@ -10,3 +10,4 @@
    1.13  time_use_thy "Pointer_Examples";
    1.14  time_use_thy "Pointer_ExamplesAbort";
    1.15  time_use_thy "SchorrWaite";
    1.16 +time_use_thy "Separation";