--- a/src/HOL/ex/ROOT.ML Wed Mar 10 22:37:33 2004 +0100 +++ b/src/HOL/ex/ROOT.ML Wed Mar 10 22:39:12 2004 +0100 @@ -39,3 +39,5 @@ time_use_thy "SVC_Oracle"; if_svc_enabled time_use_thy "svc_test"; + +time_use_thy "Refute_Examples.thy";