1 (* Title: HOL/Hoare/ROOT.ML
2 ID: $Id$
3 Author: Tobias Nipkow
4 Copyright 1998-2003 TUM
5 *)
6
7 use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples",
8 "Pointer_ExamplesAbort", "SchorrWaite", "Separation"];