(* 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"];