diff -r 5fdd4da11d49 -r 7bdc4699ef4d src/HOL/Hoare/ROOT.ML --- a/src/HOL/Hoare/ROOT.ML Tue Nov 21 17:59:45 1995 +0100 +++ b/src/HOL/Hoare/ROOT.ML Wed Nov 22 18:48:56 1995 +0100 @@ -7,3 +7,4 @@ HOL_build_completed; (*Make examples fail if HOL did*) use_thy "Examples"; +use_thy "List_Examples";