# HG changeset patch
# User wenzelm
# Date 921154835 -3600
# Node ID f7750d816c2158c745e6cf4e5fbff2a11d97134a
# Parent  fdcbeaddd5fc1d94db4e18e97ff2458f1c828df0
removed foo_build_completed -- now handled by session management (via usedir);

diff -r fdcbeaddd5fc -r f7750d816c21 src/CCL/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/CCL/ex/ROOT.ML
--- 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;
 
diff -r fdcbeaddd5fc -r f7750d816c21 src/CTT/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/CTT/ex/ROOT.ML
--- 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;
 
diff -r fdcbeaddd5fc -r f7750d816c21 src/Cube/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/Cube/ex/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/FOL/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/FOL/ex/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/FOLP/ROOT.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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/FOLP/ex/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Auth/ROOT.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";
-
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Hoare/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/IMP/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Induct/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Lambda/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Lex/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/MiniML/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Quot/ROOT.ML
--- 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";
-
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Real/ROOT.ML
--- 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;
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/Subst/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/TLA/ROOT.ML
--- 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 = ();
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/UNITY/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/W0/ROOT.ML
--- 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];
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOL/ex/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOLCF/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/HOLCF/ex/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/LCF/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/LCF/ex/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/Sequents/ILL/ROOT.ML
--- 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;
diff -r fdcbeaddd5fc -r f7750d816c21 src/Sequents/LK/ROOT.ML
--- 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;
diff -r fdcbeaddd5fc -r f7750d816c21 src/Sequents/Modal/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/Sequents/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/AC/ROOT.ML
--- 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;
 
diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/Coind/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/IMP/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/ROOT.ML
--- 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*)
diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/Resid/ROOT.ML
--- 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";
diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/ex/ROOT.ML
--- 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;