changeset 35316 | 870dfea4f9c0 |
parent 24584 | 01e83ffa6c54 |
--- a/src/HOL/Hoare/ROOT.ML Tue Feb 23 10:11:12 2010 +0100 +++ b/src/HOL/Hoare/ROOT.ML Tue Feb 23 10:11:15 2010 +0100 @@ -1,8 +1,2 @@ -(* Title: HOL/Hoare/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1998-2003 TUM -*) -use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples", - "Pointer_ExamplesAbort", "SchorrWaite", "Separation"]; +use_thy "Hoare";