changeset 14028 | ff6eb32b30a1 |
parent 13875 | 12997e3ddd8d |
child 24104 | 719fbe4fb77f |
--- a/src/HOL/Hoare/ROOT.ML Wed May 14 11:15:18 2003 +0200 +++ b/src/HOL/Hoare/ROOT.ML Wed May 14 14:20:55 2003 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/IMP/ROOT.ML ID: $Id$ Author: Tobias Nipkow - Copyright 1998 TUM + Copyright 1998-2003 TUM *) time_use_thy "Examples"; @@ -10,3 +10,4 @@ time_use_thy "Pointer_Examples"; time_use_thy "Pointer_ExamplesAbort"; time_use_thy "SchorrWaite"; +time_use_thy "Separation";