--- a/src/CCL/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/CCL/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -39,5 +39,3 @@
use_thy "Fix";
print_depth 8;
-
-val CCL_build_completed = (); (*indicate successful build*)
--- a/src/CCL/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/CCL/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Executes all examples for Classical Computational Logic
*)
-CCL_build_completed; (*Cause examples to fail if CCL did*)
-
writeln"Root file for CCL examples";
set proof_timing;
--- a/src/CTT/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/CTT/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -19,5 +19,3 @@
use_thy "Bool";
print_depth 8;
-
-val CTT_build_completed = (); (*indicate successful build*)
--- a/src/CTT/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/CTT/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -8,8 +8,6 @@
writeln"Root file for CTT examples";
-CTT_build_completed; (*Cause examples to fail if CTT did*)
-
print_depth 2;
set proof_timing;
--- a/src/Cube/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/Cube/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -14,5 +14,3 @@
use_thy "Cube";
print_depth 8;
-
-val Cube_build_completed = (); (*indicate successful build*)
--- a/src/Cube/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/Cube/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -1,7 +1,5 @@
writeln"Root file for Cube examples";
-Cube_build_completed; (*Cause examples to fail if Cube did*)
set proof_timing;
-
use_thy "ex";
--- a/src/FOL/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/FOL/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -59,5 +59,3 @@
print_depth 8;
-
-val FOL_build_completed = (); (*indicate successful build*)
--- a/src/FOL/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/FOL/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -8,8 +8,6 @@
writeln"Root file for FOL examples";
-FOL_build_completed; (*Cause examples to fail if FOL did*)
-
set proof_timing;
time_use "intro.ML";
--- a/src/FOLP/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/FOLP/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -78,5 +78,3 @@
print_depth 8;
-
-val FOLP_build_completed = (); (*indicate successful build*)
--- a/src/FOLP/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/FOLP/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -8,8 +8,6 @@
writeln"Root file for FOLP examples";
-FOLP_build_completed; (*Cause examples to fail if FOLP did*)
-
set proof_timing;
time_use "intro.ML";
--- a/src/HOL/Auth/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Auth/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,8 @@
Root file for protocol proofs.
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
+writeln"Root file for HOL/Auth";
-writeln"Root file for HOL/Auth";
set proof_timing;
goals_limit := 1;
HOL_quantifiers := false;
@@ -28,4 +27,3 @@
time_use_thy "NS_Public_Bad";
time_use_thy "NS_Public";
time_use_thy "TLS";
-
--- a/src/HOL/Hoare/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Hoare/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -4,6 +4,4 @@
Copyright 1998 TUM
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
use_thy "Examples";
--- a/src/HOL/IMP/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/IMP/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -4,9 +4,8 @@
Copyright 1995 TUM
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
+writeln"Root file for HOL/IMP";
-writeln"Root file for HOL/IMP";
set proof_timing;
time_use_thy "Expr";
time_use_thy "Transition";
--- a/src/HOL/Induct/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Induct/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,8 @@
Examples of Inductive and Coinductive Definitions
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
+writeln"Root file for HOL/Induct";
-writeln"Root file for HOL/Induct";
set proof_timing;
time_use_thy "Perm";
time_use_thy "Comb";
--- a/src/HOL/Lambda/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Lambda/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -4,8 +4,6 @@
Copyright 1998 TUM
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
writeln"Root file for HOL/Lambda";
time_use_thy "Eta";
--- a/src/HOL/Lex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Lex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -4,8 +4,6 @@
Copyright 1998 TUM
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
use_thy"AutoChopper";
use_thy"AutoChopper1";
use_thy"AutoMaxChop";
--- a/src/HOL/MiniML/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/MiniML/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Type inference for MiniML
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
writeln"Root file for HOL/MiniML";
time_use_thy "W";
--- a/src/HOL/Quot/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Quot/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,6 @@
Higher-order quotients.
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
writeln"Root file for HOL/Quot";
use_thy "FRACT";
-
--- a/src/HOL/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -76,5 +76,3 @@
print_depth 8;
Goal "True"; (*leave subgoal package empty*)
-
-val HOL_build_completed = (); (*indicate successful build*)
--- a/src/HOL/Real/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Real/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
writeln"Root file for HOL/Real";
set proof_timing;
--- a/src/HOL/Subst/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Subst/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -26,9 +26,8 @@
also loaded.
*)
-HOL_build_completed; (*Cause examples to fail if HOL did*)
+writeln"Root file for Substitutions and Unification";
-writeln"Root file for Substitutions and Unification";
use_thy "Unify";
writeln"END: Root file for Substitutions and Unification";
--- a/src/HOL/TLA/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/TLA/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,5 +6,3 @@
val banner = "Temporal Logic of Actions";
use_thy "TLA";
-
-val TLA_build_completed = ();
--- a/src/HOL/UNITY/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/UNITY/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,8 @@
Root file for UNITY proofs.
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
+writeln"Root file for HOL/UNITY";
-writeln"Root file for HOL/UNITY";
set proof_timing;
add_path "../Lex"; (*to find Prefix.thy*)
--- a/src/HOL/W0/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/W0/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,8 @@
Type inference for let-free MiniML
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
+writeln"Root file for HOL/W0";
-writeln"Root file for HOL/W0";
Unify.trace_bound := 20;
AddSEs [less_SucE];
--- a/src/HOL/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,8 @@
Executes miscellaneous examples for Higher-Order Logic.
*)
-HOL_build_completed; (*Cause examples to fail if HOL did*)
+writeln "Root file for HOL examples";
-writeln "Root file for HOL examples";
set proof_timing;
(*some examples of recursive function definitions: the TFL package*)
--- a/src/HOLCF/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOLCF/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -7,8 +7,6 @@
Should be executed in subdirectory HOLCF.
*)
-HOL_build_completed; (* Cause HOLCF to fail if HOL did *)
-
val banner = "HOLCF";
writeln banner;
@@ -28,5 +26,3 @@
use "domain/interface.ML";
print_depth 10;
-
-val HOLCF_build_completed = (); (*indicate successful build*)
--- a/src/HOLCF/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOLCF/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,11 +6,9 @@
Executes all examples for HOLCF.
*)
-HOLCF_build_completed; (*Cause examples to fail if HOLCF did*)
+writeln"Root file for HOLCF examples";
-writeln"Root file for HOLCF examples";
set proof_timing;
-
time_use_thy "Dnat";
time_use_thy "Stream";
time_use_thy "Dagstuhl";
--- a/src/LCF/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/LCF/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -16,5 +16,3 @@
use"simpdata.ML";
use_thy"pair";
use_thy"fix";
-
-val LCF_build_completed = (); (*indicate successful build*)
--- a/src/LCF/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/LCF/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -7,10 +7,8 @@
*)
writeln"Root file for LCF examples";
-LCF_build_completed; (*Cause examples to fail if LCF did*)
set proof_timing;
-
use_thy "Ex1";
use_thy "Ex2";
use_thy "Ex3";
--- a/src/Sequents/ILL/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/Sequents/ILL/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -1,5 +1,4 @@
-Sequents_build_completed; (*Cause examples to fail if Sequents did*)
writeln"Root file for ILL examples";
set proof_timing;
--- a/src/Sequents/LK/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/Sequents/LK/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Executes all examples for Classical Logic.
*)
-Sequents_build_completed; (*Cause examples to fail if Sequents did*)
-
writeln"Root file for LK examples";
set proof_timing;
--- a/src/Sequents/Modal/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/Sequents/Modal/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -4,8 +4,6 @@
Copyright 1991 University of Cambridge
*)
-Sequents_build_completed; (*Cause examples to fail if Sequents did*)
-
set proof_timing;
writeln "\nTheorems of T\n";
--- a/src/Sequents/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/Sequents/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -23,5 +23,3 @@
use_thy"S43";
print_depth 8;
-
-val Sequents_build_completed = (); (*indicate successful build*)
--- a/src/ZF/AC/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/AC/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
*)
-ZF_build_completed; (*Make examples fail if ZF did*)
-
writeln"Root file for ZF/AC";
set proof_timing;
--- a/src/ZF/Coind/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/Coind/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -13,9 +13,7 @@
Report, Computer Lab, University of Cambridge (1995).
*)
-ZF_build_completed; (*Make examples fail if ZF did*)
+writeln"Root file for ZF/Coind";
-writeln"Root file for ZF/Coind";
set proof_timing;
-
time_use_thy "MT";
--- a/src/ZF/IMP/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/IMP/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -12,9 +12,7 @@
*)
-ZF_build_completed; (*Make examples fail if ZF did*)
+writeln"Root file for ZF/IMP";
-writeln"Root file for ZF/IMP";
set proof_timing;
-
time_use_thy "Equiv";
--- a/src/ZF/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -47,5 +47,3 @@
print_depth 8;
Goal "True"; (*leave subgoal package empty*)
-
-val ZF_build_completed = (); (*indicate successful build*)
--- a/src/ZF/Resid/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/Resid/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -12,11 +12,9 @@
J. Functional Programming 4(3) 1994, 371-394.
*)
-ZF_build_completed; (*Make examples fail if ZF did*)
+writeln"Root file for ZF/Resid";
-writeln"Root file for ZF/Resid";
set proof_timing;
-
time_use_thy "Conversion";
writeln"END: Root file for ZF/Resid";
--- a/src/ZF/ex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/ex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
*)
-ZF_build_completed; (*Make examples fail if ZF did*)
-
writeln"Root file for ZF Set Theory examples";
set proof_timing;