Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed the "exit 1" calls, since now the
authorlcp
Thu, 06 Apr 1995 11:27:54 +0200
changeset 241 b67c8e01ae04
parent 240 2209eb5bb56b
child 242 8cd051d5cf74
Removed the "exit 1" calls, since now the Makefile does them.
IMP/ROOT.ML file | annotate | diff | comparison | revisions
IOA/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/IMP/ROOT.ML	Thu Apr 06 11:24:11 1995 +0200
+++ b/IMP/ROOT.ML	Thu Apr 06 11:27:54 1995 +0200
@@ -17,6 +17,5 @@
 writeln"Root file for HOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-(time_use_thy "Properties";
- time_use_thy "Equiv"
-)  handle _ => exit 1;
+time_use_thy "Properties";
+time_use_thy "Equiv";
--- a/IOA/ROOT.ML	Thu Apr 06 11:24:11 1995 +0200
+++ b/IOA/ROOT.ML	Thu Apr 06 11:27:54 1995 +0200
@@ -19,4 +19,4 @@
 goals_limit := 1;
 
 loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
-use_thy "Correctness"  handle _ => exit 1;
+use_thy "Correctness";
Old_HOL