added exit 1
authornipkow
Tue, 14 Mar 1995 09:47:28 +0100
changeset 951 682139612060
parent 950 323f8ca4587a
child 952 9e10962866b0
added exit 1
src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Mon Mar 13 09:42:50 1995 +0100
+++ b/src/HOL/IMP/ROOT.ML	Tue Mar 14 09:47:28 1995 +0100
@@ -19,6 +19,7 @@
 writeln"Root file for CHOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-time_use_thy "Properties";
-time_use_thy "Equiv";
-time_use_thy "Hoare";
+(time_use_thy "Properties";
+ time_use_thy "Equiv";
+ time_use_thy "Hoare"
+) handle _ => exit 1;