removed foo_build_completed -- now handled by session management (via usedir);
authorwenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349f7750d816c21
parent 6348 fdcbeaddd5fc
child 6350 b5f1f861155d
removed foo_build_completed -- now handled by session management (via usedir);
src/CCL/ROOT.ML
src/CCL/ex/ROOT.ML
src/CTT/ROOT.ML
src/CTT/ex/ROOT.ML
src/Cube/ROOT.ML
src/Cube/ex/ROOT.ML
src/FOL/ROOT.ML
src/FOL/ex/ROOT.ML
src/FOLP/ROOT.ML
src/FOLP/ex/ROOT.ML
src/HOL/Auth/ROOT.ML
src/HOL/Hoare/ROOT.ML
src/HOL/IMP/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/Lambda/ROOT.ML
src/HOL/Lex/ROOT.ML
src/HOL/MiniML/ROOT.ML
src/HOL/Quot/ROOT.ML
src/HOL/ROOT.ML
src/HOL/Real/ROOT.ML
src/HOL/Subst/ROOT.ML
src/HOL/TLA/ROOT.ML
src/HOL/UNITY/ROOT.ML
src/HOL/W0/ROOT.ML
src/HOL/ex/ROOT.ML
src/HOLCF/ROOT.ML
src/HOLCF/ex/ROOT.ML
src/LCF/ROOT.ML
src/LCF/ex/ROOT.ML
src/Sequents/ILL/ROOT.ML
src/Sequents/LK/ROOT.ML
src/Sequents/Modal/ROOT.ML
src/Sequents/ROOT.ML
src/ZF/AC/ROOT.ML
src/ZF/Coind/ROOT.ML
src/ZF/IMP/ROOT.ML
src/ZF/ROOT.ML
src/ZF/Resid/ROOT.ML
src/ZF/ex/ROOT.ML
     1.1 --- a/src/CCL/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     1.2 +++ b/src/CCL/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     1.3 @@ -39,5 +39,3 @@
     1.4  use_thy "Fix";
     1.5  
     1.6  print_depth 8;
     1.7 -
     1.8 -val CCL_build_completed = ();   (*indicate successful build*)
     2.1 --- a/src/CCL/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     2.2 +++ b/src/CCL/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     2.3 @@ -6,8 +6,6 @@
     2.4  Executes all examples for Classical Computational Logic
     2.5  *)
     2.6  
     2.7 -CCL_build_completed;    (*Cause examples to fail if CCL did*)
     2.8 -
     2.9  writeln"Root file for CCL examples";
    2.10  set proof_timing;
    2.11  
     3.1 --- a/src/CTT/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     3.2 +++ b/src/CTT/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     3.3 @@ -19,5 +19,3 @@
     3.4  use_thy "Bool";
     3.5  
     3.6  print_depth 8;
     3.7 -
     3.8 -val CTT_build_completed = ();   (*indicate successful build*)
     4.1 --- a/src/CTT/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     4.2 +++ b/src/CTT/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     4.3 @@ -8,8 +8,6 @@
     4.4  
     4.5  writeln"Root file for CTT examples";
     4.6  
     4.7 -CTT_build_completed;    (*Cause examples to fail if CTT did*)
     4.8 -
     4.9  print_depth 2;  
    4.10  set proof_timing;
    4.11  
     5.1 --- a/src/Cube/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     5.2 +++ b/src/Cube/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     5.3 @@ -14,5 +14,3 @@
     5.4  use_thy "Cube";
     5.5  
     5.6  print_depth 8;
     5.7 -
     5.8 -val Cube_build_completed = ();  (*indicate successful build*)
     6.1 --- a/src/Cube/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     6.2 +++ b/src/Cube/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     6.3 @@ -1,7 +1,5 @@
     6.4  
     6.5  writeln"Root file for Cube examples";
     6.6 -Cube_build_completed;    (*Cause examples to fail if Cube did*)
     6.7  
     6.8  set proof_timing;
     6.9 -
    6.10  use_thy "ex";
     7.1 --- a/src/FOL/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     7.2 +++ b/src/FOL/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     7.3 @@ -59,5 +59,3 @@
     7.4  
     7.5  
     7.6  print_depth 8;
     7.7 -
     7.8 -val FOL_build_completed = ();   (*indicate successful build*)
     8.1 --- a/src/FOL/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     8.2 +++ b/src/FOL/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     8.3 @@ -8,8 +8,6 @@
     8.4  
     8.5  writeln"Root file for FOL examples";
     8.6  
     8.7 -FOL_build_completed;    (*Cause examples to fail if FOL did*)
     8.8 -
     8.9  set proof_timing;
    8.10  
    8.11  time_use     "intro.ML";
     9.1 --- a/src/FOLP/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
     9.2 +++ b/src/FOLP/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
     9.3 @@ -78,5 +78,3 @@
     9.4  
     9.5  
     9.6  print_depth 8;
     9.7 -
     9.8 -val FOLP_build_completed = ();  (*indicate successful build*)
    10.1 --- a/src/FOLP/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    10.2 +++ b/src/FOLP/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    10.3 @@ -8,8 +8,6 @@
    10.4  
    10.5  writeln"Root file for FOLP examples";
    10.6  
    10.7 -FOLP_build_completed;   (*Cause examples to fail if FOLP did*)
    10.8 -
    10.9  set proof_timing;
   10.10  
   10.11  time_use     "intro.ML";
    11.1 --- a/src/HOL/Auth/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    11.2 +++ b/src/HOL/Auth/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    11.3 @@ -6,9 +6,8 @@
    11.4  Root file for protocol proofs.
    11.5  *)
    11.6  
    11.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    11.8 +writeln"Root file for HOL/Auth";
    11.9  
   11.10 -writeln"Root file for HOL/Auth";
   11.11  set proof_timing;
   11.12  goals_limit := 1;
   11.13  HOL_quantifiers := false;
   11.14 @@ -28,4 +27,3 @@
   11.15  time_use_thy "NS_Public_Bad";
   11.16  time_use_thy "NS_Public";
   11.17  time_use_thy "TLS";
   11.18 -
    12.1 --- a/src/HOL/Hoare/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    12.2 +++ b/src/HOL/Hoare/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    12.3 @@ -4,6 +4,4 @@
    12.4      Copyright   1998 TUM
    12.5  *)
    12.6  
    12.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    12.8 -
    12.9  use_thy "Examples";
    13.1 --- a/src/HOL/IMP/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    13.2 +++ b/src/HOL/IMP/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    13.3 @@ -4,9 +4,8 @@
    13.4      Copyright   1995 TUM
    13.5  *)
    13.6  
    13.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    13.8 +writeln"Root file for HOL/IMP";
    13.9  
   13.10 -writeln"Root file for HOL/IMP";
   13.11  set proof_timing;
   13.12  time_use_thy "Expr";
   13.13  time_use_thy "Transition";
    14.1 --- a/src/HOL/Induct/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    14.2 +++ b/src/HOL/Induct/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    14.3 @@ -6,9 +6,8 @@
    14.4  Examples of Inductive and Coinductive Definitions
    14.5  *)
    14.6  
    14.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    14.8 +writeln"Root file for HOL/Induct";
    14.9  
   14.10 -writeln"Root file for HOL/Induct";
   14.11  set proof_timing;
   14.12  time_use_thy "Perm";
   14.13  time_use_thy "Comb";
    15.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    15.2 +++ b/src/HOL/Lambda/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    15.3 @@ -4,8 +4,6 @@
    15.4      Copyright   1998 TUM
    15.5  *)
    15.6  
    15.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    15.8 -
    15.9  writeln"Root file for HOL/Lambda";
   15.10  
   15.11  time_use_thy "Eta";
    16.1 --- a/src/HOL/Lex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    16.2 +++ b/src/HOL/Lex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    16.3 @@ -4,8 +4,6 @@
    16.4      Copyright   1998 TUM
    16.5  *)
    16.6  
    16.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    16.8 -
    16.9  use_thy"AutoChopper";
   16.10  use_thy"AutoChopper1";
   16.11  use_thy"AutoMaxChop";
    17.1 --- a/src/HOL/MiniML/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    17.2 +++ b/src/HOL/MiniML/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    17.3 @@ -6,8 +6,6 @@
    17.4  Type inference for MiniML
    17.5  *)
    17.6  
    17.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    17.8 -
    17.9  writeln"Root file for HOL/MiniML";
   17.10  
   17.11  time_use_thy "W";
    18.1 --- a/src/HOL/Quot/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    18.2 +++ b/src/HOL/Quot/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    18.3 @@ -6,9 +6,6 @@
    18.4  Higher-order quotients.
    18.5  *)
    18.6  
    18.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    18.8 -
    18.9  writeln"Root file for HOL/Quot";
   18.10  
   18.11  use_thy "FRACT";
   18.12 -
    19.1 --- a/src/HOL/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    19.2 +++ b/src/HOL/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    19.3 @@ -76,5 +76,3 @@
    19.4  print_depth 8;
    19.5  
    19.6  Goal "True";  (*leave subgoal package empty*)
    19.7 -
    19.8 -val HOL_build_completed = ();   (*indicate successful build*)
    20.1 --- a/src/HOL/Real/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    20.2 +++ b/src/HOL/Real/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    20.3 @@ -6,8 +6,6 @@
    20.4  Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
    20.5  *)
    20.6  
    20.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    20.8 -
    20.9  writeln"Root file for HOL/Real";
   20.10  
   20.11  set proof_timing;
    21.1 --- a/src/HOL/Subst/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    21.2 +++ b/src/HOL/Subst/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    21.3 @@ -26,9 +26,8 @@
    21.4  also loaded. 
    21.5  *)
    21.6  
    21.7 -HOL_build_completed;    (*Cause examples to fail if HOL did*)
    21.8 +writeln"Root file for Substitutions and Unification";
    21.9  
   21.10 -writeln"Root file for Substitutions and Unification";
   21.11  use_thy "Unify";
   21.12  
   21.13  writeln"END: Root file for Substitutions and Unification";
    22.1 --- a/src/HOL/TLA/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    22.2 +++ b/src/HOL/TLA/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    22.3 @@ -6,5 +6,3 @@
    22.4  val banner = "Temporal Logic of Actions";
    22.5  
    22.6  use_thy "TLA";
    22.7 -
    22.8 -val TLA_build_completed = ();
    23.1 --- a/src/HOL/UNITY/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    23.2 +++ b/src/HOL/UNITY/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    23.3 @@ -6,9 +6,8 @@
    23.4  Root file for UNITY proofs.
    23.5  *)
    23.6  
    23.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    23.8 +writeln"Root file for HOL/UNITY";
    23.9  
   23.10 -writeln"Root file for HOL/UNITY";
   23.11  set proof_timing;
   23.12  
   23.13  add_path "../Lex";	(*to find Prefix.thy*)
    24.1 --- a/src/HOL/W0/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    24.2 +++ b/src/HOL/W0/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    24.3 @@ -6,9 +6,8 @@
    24.4  Type inference for let-free MiniML
    24.5  *)
    24.6  
    24.7 -HOL_build_completed;    (*Make examples fail if HOL did*)
    24.8 +writeln"Root file for HOL/W0";
    24.9  
   24.10 -writeln"Root file for HOL/W0";
   24.11  Unify.trace_bound := 20;
   24.12  
   24.13  AddSEs [less_SucE];
    25.1 --- a/src/HOL/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    25.2 +++ b/src/HOL/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    25.3 @@ -6,9 +6,8 @@
    25.4  Executes miscellaneous examples for Higher-Order Logic. 
    25.5  *)
    25.6  
    25.7 -HOL_build_completed;    (*Cause examples to fail if HOL did*)
    25.8 +writeln "Root file for HOL examples";
    25.9  
   25.10 -writeln "Root file for HOL examples";
   25.11  set proof_timing;
   25.12  
   25.13  (*some examples of recursive function definitions: the TFL package*)
    26.1 --- a/src/HOLCF/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    26.2 +++ b/src/HOLCF/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    26.3 @@ -7,8 +7,6 @@
    26.4  Should be executed in subdirectory HOLCF.
    26.5  *)
    26.6  
    26.7 -HOL_build_completed;    (* Cause HOLCF to fail if HOL did *)
    26.8 -
    26.9  val banner = "HOLCF";
   26.10  writeln banner;
   26.11  
   26.12 @@ -28,5 +26,3 @@
   26.13  use "domain/interface.ML";
   26.14  
   26.15  print_depth 10;  
   26.16 -
   26.17 -val HOLCF_build_completed = (); (*indicate successful build*)
    27.1 --- a/src/HOLCF/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    27.2 +++ b/src/HOLCF/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    27.3 @@ -6,11 +6,9 @@
    27.4  Executes all examples for HOLCF. 
    27.5  *)
    27.6  
    27.7 -HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
    27.8 +writeln"Root file for HOLCF examples";
    27.9  
   27.10 -writeln"Root file for HOLCF examples";
   27.11  set proof_timing;
   27.12 -
   27.13  time_use_thy "Dnat";
   27.14  time_use_thy "Stream";
   27.15  time_use_thy "Dagstuhl";
    28.1 --- a/src/LCF/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    28.2 +++ b/src/LCF/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    28.3 @@ -16,5 +16,3 @@
    28.4  use"simpdata.ML";
    28.5  use_thy"pair";
    28.6  use_thy"fix";
    28.7 -
    28.8 -val LCF_build_completed = ();   (*indicate successful build*)
    29.1 --- a/src/LCF/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    29.2 +++ b/src/LCF/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    29.3 @@ -7,10 +7,8 @@
    29.4  *)
    29.5  
    29.6  writeln"Root file for LCF examples";
    29.7 -LCF_build_completed;    (*Cause examples to fail if LCF did*)
    29.8  
    29.9  set proof_timing;
   29.10 -
   29.11  use_thy "Ex1";
   29.12  use_thy "Ex2";
   29.13  use_thy "Ex3";
    30.1 --- a/src/Sequents/ILL/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    30.2 +++ b/src/Sequents/ILL/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    30.3 @@ -1,5 +1,4 @@
    30.4  
    30.5 -Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
    30.6  writeln"Root file for ILL examples";
    30.7  
    30.8  set proof_timing;
    31.1 --- a/src/Sequents/LK/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    31.2 +++ b/src/Sequents/LK/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    31.3 @@ -6,8 +6,6 @@
    31.4  Executes all examples for Classical Logic. 
    31.5  *)
    31.6  
    31.7 -Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
    31.8 -
    31.9  writeln"Root file for LK examples";
   31.10  
   31.11  set proof_timing;
    32.1 --- a/src/Sequents/Modal/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    32.2 +++ b/src/Sequents/Modal/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    32.3 @@ -4,8 +4,6 @@
    32.4      Copyright   1991  University of Cambridge
    32.5  *)
    32.6  
    32.7 -Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
    32.8 -
    32.9  set proof_timing;
   32.10  
   32.11  writeln "\nTheorems of T\n";
    33.1 --- a/src/Sequents/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    33.2 +++ b/src/Sequents/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    33.3 @@ -23,5 +23,3 @@
    33.4  use_thy"S43";
    33.5  
    33.6  print_depth 8;
    33.7 -
    33.8 -val Sequents_build_completed = ();    (*indicate successful build*)
    34.1 --- a/src/ZF/AC/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    34.2 +++ b/src/ZF/AC/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    34.3 @@ -6,8 +6,6 @@
    34.4  Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
    34.5  *)
    34.6  
    34.7 -ZF_build_completed;     (*Make examples fail if ZF did*)
    34.8 -
    34.9  writeln"Root file for ZF/AC";
   34.10  set proof_timing;
   34.11  
    35.1 --- a/src/ZF/Coind/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    35.2 +++ b/src/ZF/Coind/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    35.3 @@ -13,9 +13,7 @@
    35.4      Report, Computer Lab, University of Cambridge (1995).
    35.5  *)
    35.6  
    35.7 -ZF_build_completed;     (*Make examples fail if ZF did*)
    35.8 +writeln"Root file for ZF/Coind";
    35.9  
   35.10 -writeln"Root file for ZF/Coind";
   35.11  set proof_timing;
   35.12 -
   35.13  time_use_thy "MT";
    36.1 --- a/src/ZF/IMP/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    36.2 +++ b/src/ZF/IMP/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    36.3 @@ -12,9 +12,7 @@
    36.4  
    36.5  *)
    36.6  
    36.7 -ZF_build_completed;     (*Make examples fail if ZF did*)
    36.8 +writeln"Root file for ZF/IMP";
    36.9  
   36.10 -writeln"Root file for ZF/IMP";
   36.11  set proof_timing;
   36.12 -
   36.13  time_use_thy "Equiv";
    37.1 --- a/src/ZF/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    37.2 +++ b/src/ZF/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    37.3 @@ -47,5 +47,3 @@
    37.4  print_depth 8;
    37.5  
    37.6  Goal "True";  (*leave subgoal package empty*)
    37.7 -
    37.8 -val ZF_build_completed = ();    (*indicate successful build*)
    38.1 --- a/src/ZF/Resid/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    38.2 +++ b/src/ZF/Resid/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    38.3 @@ -12,11 +12,9 @@
    38.4  J. Functional Programming 4(3) 1994, 371-394.
    38.5  *)
    38.6  
    38.7 -ZF_build_completed;     (*Make examples fail if ZF did*)
    38.8 +writeln"Root file for ZF/Resid";
    38.9  
   38.10 -writeln"Root file for ZF/Resid";
   38.11  set proof_timing;
   38.12 -
   38.13  time_use_thy "Conversion";
   38.14  
   38.15  writeln"END: Root file for ZF/Resid";
    39.1 --- a/src/ZF/ex/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
    39.2 +++ b/src/ZF/ex/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
    39.3 @@ -6,8 +6,6 @@
    39.4  Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
    39.5  *)
    39.6  
    39.7 -ZF_build_completed;     (*Make examples fail if ZF did*)
    39.8 -
    39.9  writeln"Root file for ZF Set Theory examples";
   39.10  set proof_timing;
   39.11