IMP/ROOT.ML

 HOL_build_completed;	(*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-time_use_thy "Properties";
-time_use_thy "Equiv";
+(time_use_thy "Properties";
+ time_use_thy "Equiv"
+)  handle _ => exit 1;