cleaned up;
authorwenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000c20d58286a51
parent 8999 ad8260dc6e4a
child 9001 93af64f54bf2
cleaned up;
Admin/Benchmarks/HOL-datatype/ROOT.ML
src/CCL/ROOT.ML
src/CCL/ex/ROOT.ML
src/CTT/ex/ROOT.ML
src/Cube/ex/ROOT.ML
src/FOL/ex/ROOT.ML
src/FOLP/ex/ROOT.ML
src/HOL/Algebra/ROOT.ML
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/ROOT.ML
src/HOL/AxClasses/Group/ROOT.ML
src/HOL/AxClasses/Lattice/ROOT.ML
src/HOL/AxClasses/Tutorial/ROOT.ML
src/HOL/BCV/ROOT.ML
src/HOL/Hoare/ROOT.ML
src/HOL/IMP/ROOT.ML
src/HOL/IMPP/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/Integ/IntArith.ML
src/HOL/Integ/NatSimprocs.ML
src/HOL/Lambda/ROOT.ML
src/HOL/Lex/ROOT.ML
src/HOL/MicroJava/ROOT.ML
src/HOL/MiniML/ROOT.ML
src/HOL/Modelcheck/ROOT.ML
src/HOL/Quot/ROOT.ML
src/HOL/Real/ROOT.ML
src/HOL/Real/ex/ROOT.ML
src/HOL/Subst/ROOT.ML
src/HOL/TLA/Buffer/ROOT.ML
src/HOL/TLA/Inc/ROOT.ML
src/HOL/TLA/Memory/ROOT.ML
src/HOL/TLA/ROOT.ML
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/UNITY.ML
src/HOL/W0/ROOT.ML
src/HOL/ex/BinEx.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/mesontest2.ML
src/HOLCF/IMP/ROOT.ML
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/Modelcheck/ROOT.ML
src/HOLCF/IOA/NTP/ROOT.ML
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/Storage/ROOT.ML
src/HOLCF/IOA/ex/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/Datatype.ML
src/ZF/IMP/ROOT.ML
src/ZF/Resid/ROOT.ML
src/ZF/ex/BinEx.ML
src/ZF/ex/ROOT.ML
     1.1 --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     1.2 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  val tests = ["Brackin", "Instructions", "SML", "Verilog"];
     1.6  
     1.7 -set Toplevel.trace;
     1.8 +set timing;
     1.9  
    1.10  warning "\nset quick_and_dirty\n"; set quick_and_dirty;
    1.11  seq time_use_thy tests;
     2.1 --- a/src/CCL/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     2.2 +++ b/src/CCL/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      CCL/ROOT
     2.5 +(*  Title:      CCL/ROOT.ML
     2.6      ID:         $Id$
     2.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     2.8      Copyright   1993  University of Cambridge
     3.1 --- a/src/CCL/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     3.2 +++ b/src/CCL/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      CCL/ex/ROOT
     3.5 +(*  Title:      CCL/ex/ROOT.ML
     3.6      ID:         $Id$
     3.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     3.8      Copyright   1993  University of Cambridge
     3.9 @@ -6,9 +6,6 @@
    3.10  Executes all examples for Classical Computational Logic
    3.11  *)
    3.12  
    3.13 -writeln"Root file for CCL examples";
    3.14 -set proof_timing;
    3.15 -
    3.16  time_use_thy "Nat";
    3.17  time_use_thy "List";
    3.18  time_use_thy "Stream";
     4.1 --- a/src/CTT/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     4.2 +++ b/src/CTT/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      CTT/ex/ROOT
     4.5 +(*  Title:      CTT/ex/ROOT.ML
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1991  University of Cambridge
     4.9 @@ -6,10 +6,7 @@
    4.10  Executes all examples for Constructive Type Theory. 
    4.11  *)
    4.12  
    4.13 -writeln"Root file for CTT examples";
    4.14 -
    4.15  print_depth 2;  
    4.16 -set proof_timing;
    4.17  
    4.18  time_use "typechk.ML";
    4.19  time_use "elim.ML";
     5.1 --- a/src/Cube/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     5.2 +++ b/src/Cube/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     5.3 @@ -1,5 +1,2 @@
     5.4  
     5.5 -writeln"Root file for Cube examples";
     5.6 -
     5.7 -set proof_timing;
     5.8 -use_thy "ex";
     5.9 +time_use_thy "ex";
     6.1 --- a/src/FOL/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     6.2 +++ b/src/FOL/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     6.3 @@ -6,10 +6,6 @@
     6.4  Executes all examples for First-Order Logic. 
     6.5  *)
     6.6  
     6.7 -writeln"Root file for FOL examples";
     6.8 -
     6.9 -set proof_timing;
    6.10 -
    6.11  time_use     "intro.ML";
    6.12  time_use_thy "Nat";
    6.13  time_use     "foundn.ML";
     7.1 --- a/src/FOLP/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     7.2 +++ b/src/FOLP/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     7.3 @@ -6,10 +6,6 @@
     7.4  Executes all examples for First-Order Logic. 
     7.5  *)
     7.6  
     7.7 -writeln"Root file for FOLP examples";
     7.8 -
     7.9 -set proof_timing;
    7.10 -
    7.11  time_use     "intro.ML";
    7.12  time_use_thy "Nat";
    7.13  time_use     "foundn.ML";
     8.1 --- a/src/HOL/Algebra/ROOT.ML	Tue May 30 16:03:09 2000 +0200
     8.2 +++ b/src/HOL/Algebra/ROOT.ML	Tue May 30 16:08:38 2000 +0200
     8.3 @@ -4,5 +4,5 @@
     8.4      Author: Clemens Ballarin, started 24 September 1999
     8.5  *)
     8.6  
     8.7 -with_path "abstract" use_thy "Abstract";        (*The ring theory*)
     8.8 -with_path "poly"     use_thy "Polynomial";      (*The full theory*)
     8.9 +with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
    8.10 +with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
     9.1 --- a/src/HOL/Auth/KerberosIV.ML	Tue May 30 16:03:09 2000 +0200
     9.2 +++ b/src/HOL/Auth/KerberosIV.ML	Tue May 30 16:08:38 2000 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  *)
     9.5  
     9.6  Pretty.setdepth 20;
     9.7 -proof_timing:=true;
     9.8 +set timing;
     9.9  
    9.10  AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
    9.11  
    10.1 --- a/src/HOL/Auth/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    10.2 +++ b/src/HOL/Auth/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    10.3 @@ -6,9 +6,6 @@
    10.4  Root file for protocol proofs.
    10.5  *)
    10.6  
    10.7 -writeln"Root file for HOL/Auth";
    10.8 -
    10.9 -set proof_timing;
   10.10  goals_limit := 1;
   10.11  
   10.12  (*Shared-key protocols*)
    11.1 --- a/src/HOL/AxClasses/Group/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    11.2 +++ b/src/HOL/AxClasses/Group/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    11.3 @@ -8,7 +8,7 @@
    11.4  set show_types;
    11.5  set show_sorts;
    11.6  
    11.7 -use_thy "Monoid";
    11.8 -use_thy "Group";
    11.9 -use_thy "MonoidGroupInsts";
   11.10 -use_thy "GroupInsts";
   11.11 +time_use_thy "Monoid";
   11.12 +time_use_thy "Group";
   11.13 +time_use_thy "MonoidGroupInsts";
   11.14 +time_use_thy "GroupInsts";
    12.1 --- a/src/HOL/AxClasses/Lattice/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    12.2 +++ b/src/HOL/AxClasses/Lattice/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    12.3 @@ -11,14 +11,14 @@
    12.4  set show_types;
    12.5  set show_sorts;
    12.6  
    12.7 -use_thy "Order";
    12.8 -use_thy "OrdDefs";
    12.9 -use_thy "OrdInsts";
   12.10 +time_use_thy "Order";
   12.11 +time_use_thy "OrdDefs";
   12.12 +time_use_thy "OrdInsts";
   12.13  
   12.14 -use_thy "Lattice";
   12.15 -use_thy "CLattice";
   12.16 +time_use_thy "Lattice";
   12.17 +time_use_thy "CLattice";
   12.18  
   12.19 -use_thy "LatPreInsts";
   12.20 -use_thy "LatInsts";
   12.21 +time_use_thy "LatPreInsts";
   12.22 +time_use_thy "LatInsts";
   12.23  
   12.24 -use_thy "LatMorph";
   12.25 +time_use_thy "LatMorph";
    13.1 --- a/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    13.2 +++ b/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4  
    13.5 -use_thy "Semigroups";
    13.6 -use_thy "Group";
    13.7 -use_thy "Product";
    13.8 +time_use_thy "Semigroups";
    13.9 +time_use_thy "Group";
   13.10 +time_use_thy "Product";
    14.1 --- a/src/HOL/BCV/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    14.2 +++ b/src/HOL/BCV/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    14.3 @@ -7,6 +7,4 @@
    14.4  aka `bytecode verification'.
    14.5  *)
    14.6  
    14.7 -writeln"Root file for HOL/BCV";
    14.8 -
    14.9  time_use_thy "Machine";
    15.1 --- a/src/HOL/Hoare/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    15.2 +++ b/src/HOL/Hoare/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    15.3 @@ -4,4 +4,4 @@
    15.4      Copyright   1998 TUM
    15.5  *)
    15.6  
    15.7 -use_thy "Examples";
    15.8 +time_use_thy "Examples";
    16.1 --- a/src/HOL/IMP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    16.2 +++ b/src/HOL/IMP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    16.3 @@ -4,9 +4,6 @@
    16.4      Copyright   1995 TUM
    16.5  *)
    16.6  
    16.7 -writeln"Root file for HOL/IMP";
    16.8 -
    16.9 -set proof_timing;
   16.10  time_use_thy "Expr";
   16.11  time_use_thy "Transition";
   16.12  time_use_thy "VC";
    17.1 --- a/src/HOL/IMPP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    17.2 +++ b/src/HOL/IMPP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    17.3 @@ -4,6 +4,4 @@
    17.4      Copyright   1999 TUM
    17.5  *)
    17.6  
    17.7 -writeln"Root file for HOL/IMPP";
    17.8 -
    17.9 -use_thy "EvenOdd";
   17.10 +time_use_thy "EvenOdd";
    18.1 --- a/src/HOL/Induct/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    18.2 +++ b/src/HOL/Induct/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    18.3 @@ -6,9 +6,6 @@
    18.4  Examples of Inductive and Coinductive Definitions
    18.5  *)
    18.6  
    18.7 -writeln"Root file for HOL/Induct";
    18.8 -
    18.9 -set proof_timing;
   18.10  time_use_thy "Perm";
   18.11  time_use_thy "Comb";
   18.12  time_use_thy "Mutil";
    19.1 --- a/src/HOL/Integ/IntArith.ML	Tue May 30 16:03:09 2000 +0200
    19.2 +++ b/src/HOL/Integ/IntArith.ML	Tue May 30 16:08:38 2000 +0200
    19.3 @@ -308,7 +308,7 @@
    19.4  
    19.5  (*examples:
    19.6  print_depth 22;
    19.7 -set proof_timing;
    19.8 +set timing;
    19.9  set trace_simp;
   19.10  fun test s = (Goal s; by (Simp_tac 1)); 
   19.11  
    20.1 --- a/src/HOL/Integ/NatSimprocs.ML	Tue May 30 16:03:09 2000 +0200
    20.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Tue May 30 16:08:38 2000 +0200
    20.3 @@ -287,7 +287,7 @@
    20.4  
    20.5  (*examples:
    20.6  print_depth 22;
    20.7 -set proof_timing;
    20.8 +set timing;
    20.9  set trace_simp;
   20.10  fun test s = (Goal s; by (Simp_tac 1)); 
   20.11  
    21.1 --- a/src/HOL/Lambda/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    21.2 +++ b/src/HOL/Lambda/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    21.3 @@ -4,8 +4,6 @@
    21.4      Copyright   1998 TUM
    21.5  *)
    21.6  
    21.7 -writeln"Root file for HOL/Lambda";
    21.8 -
    21.9  time_use_thy "Eta";
   21.10 -time_use_thy "../Induct/Acc";
   21.11 +with_path "../Induct" time_use_thy "Acc";
   21.12  time_use_thy "InductTermi";
    22.1 --- a/src/HOL/Lex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    22.2 +++ b/src/HOL/Lex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    22.3 @@ -4,8 +4,8 @@
    22.4      Copyright   1998 TUM
    22.5  *)
    22.6  
    22.7 -use_thy"AutoChopper";
    22.8 -use_thy"AutoChopper1";
    22.9 -use_thy"AutoMaxChop";
   22.10 -use_thy"RegSet_of_nat_DA";
   22.11 -use_thy"Scanner";
   22.12 +time_use_thy "AutoChopper";
   22.13 +time_use_thy "AutoChopper1";
   22.14 +time_use_thy "AutoMaxChop";
   22.15 +time_use_thy "RegSet_of_nat_DA";
   22.16 +time_use_thy "Scanner";
    23.1 --- a/src/HOL/MicroJava/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    23.2 +++ b/src/HOL/MicroJava/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    23.3 @@ -1,12 +1,8 @@
    23.4 +
    23.5  goals_limit:=1;
    23.6  
    23.7  Unify.search_bound := 40;
    23.8  Unify.trace_bound  := 40;
    23.9  
   23.10 -add_path "J";
   23.11 -add_path "JVM";
   23.12 -add_path "BV";
   23.13 -
   23.14 -
   23.15 -use_thy "JTypeSafe";
   23.16 -use_thy "BVSpecTypeSafe";
   23.17 +with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "JTypeSafe";
   23.18 +with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "BVSpecTypeSafe";
    24.1 --- a/src/HOL/MiniML/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    24.2 +++ b/src/HOL/MiniML/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    24.3 @@ -6,6 +6,4 @@
    24.4  Type inference for MiniML
    24.5  *)
    24.6  
    24.7 -writeln"Root file for HOL/MiniML";
    24.8 -
    24.9  time_use_thy "W";
    25.1 --- a/src/HOL/Modelcheck/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    25.2 +++ b/src/HOL/Modelcheck/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    25.3 @@ -8,16 +8,16 @@
    25.4  
    25.5  (* Mucke -- mu-calculus model checker from Karlsruhe *)
    25.6  
    25.7 -use "mucke_oracle.ML";
    25.8 -use_thy "MuckeSyn";
    25.9 +time_use "mucke_oracle.ML";
   25.10 +time_use_thy "MuckeSyn";
   25.11  
   25.12 -if_mucke_enabled use_thy "MuckeExample1";
   25.13 -if_mucke_enabled use_thy "MuckeExample2";
   25.14 +if_mucke_enabled time_use_thy "MuckeExample1";
   25.15 +if_mucke_enabled time_use_thy "MuckeExample2";
   25.16  
   25.17  
   25.18  (* Einhoven model checker *)
   25.19  
   25.20 -use_thy "CTL";
   25.21 -use_thy "EindhovenSyn";
   25.22 +time_use_thy "CTL";
   25.23 +time_use_thy "EindhovenSyn";
   25.24  
   25.25 -if_eindhoven_enabled use_thy "EindhovenExample";
   25.26 +if_eindhoven_enabled time_use_thy "EindhovenExample";
    26.1 --- a/src/HOL/Quot/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    26.2 +++ b/src/HOL/Quot/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    26.3 @@ -1,11 +1,7 @@
    26.4  (*  Title:      HOL/Quot/ROOT.ML
    26.5      ID:         $Id$
    26.6 -    Author:     
    26.7 -    Copyright   
    26.8  
    26.9  Higher-order quotients.
   26.10  *)
   26.11  
   26.12 -writeln"Root file for HOL/Quot";
   26.13 -
   26.14 -use_thy "FRACT";
   26.15 +time_use_thy "FRACT";
    27.1 --- a/src/HOL/Real/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    27.2 +++ b/src/HOL/Real/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    27.3 @@ -8,8 +8,6 @@
    27.4  Linear real arithmetic is installed in RealBin.ML.
    27.5  *)
    27.6  
    27.7 -writeln"Root file for HOL/Real";
    27.8 -
    27.9  time_use_thy "RealDef";
   27.10  use          "simproc.ML";
   27.11  time_use_thy "Real";
    28.1 --- a/src/HOL/Real/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    28.2 +++ b/src/HOL/Real/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    28.3 @@ -6,8 +6,4 @@
    28.4  HOL/Real examples.
    28.5  *)
    28.6  
    28.7 -writeln "Root file for HOL/Real examples";
    28.8 -
    28.9 -set proof_timing;
   28.10 -
   28.11  time_use_thy "BinEx";
    29.1 --- a/src/HOL/Subst/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    29.2 +++ b/src/HOL/Subst/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    29.3 @@ -22,12 +22,6 @@
    29.4                  correctness and termination
    29.5  Unify        -  the unification function
    29.6  
    29.7 -To load, type use"ROOT.ML"; into an Isabelle-HOL that has TFL 
    29.8 -also loaded. 
    29.9  *)
   29.10  
   29.11 -writeln"Root file for Substitutions and Unification";
   29.12 -
   29.13 -use_thy "Unify";
   29.14 -
   29.15 -writeln"END: Root file for Substitutions and Unification";
   29.16 +time_use_thy "Unify";
    30.1 --- a/src/HOL/TLA/Buffer/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    30.2 +++ b/src/HOL/TLA/Buffer/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    30.3 @@ -1,2 +1,2 @@
    30.4  
    30.5 -use_thy "DBuffer";
    30.6 +time_use_thy "DBuffer";
    31.1 --- a/src/HOL/TLA/Inc/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    31.2 +++ b/src/HOL/TLA/Inc/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    31.3 @@ -1,2 +1,2 @@
    31.4  
    31.5 -use_thy "Inc";
    31.6 +time_use_thy "Inc";
    32.1 --- a/src/HOL/TLA/Memory/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    32.2 +++ b/src/HOL/TLA/Memory/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    32.3 @@ -1,2 +1,2 @@
    32.4  
    32.5 -use_thy "MemoryImplementation";
    32.6 +time_use_thy "MemoryImplementation";
    33.1 --- a/src/HOL/TLA/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    33.2 +++ b/src/HOL/TLA/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    33.3 @@ -5,4 +5,4 @@
    33.4  
    33.5  val banner = "Temporal Logic of Actions";
    33.6  
    33.7 -use_thy "TLA";
    33.8 +time_use_thy "TLA";
    34.1 --- a/src/HOL/UNITY/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    34.2 +++ b/src/HOL/UNITY/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    34.3 @@ -6,10 +6,6 @@
    34.4  Root file for UNITY proofs.
    34.5  *)
    34.6  
    34.7 -writeln"Root file for HOL/UNITY";
    34.8 -
    34.9 -set proof_timing;
   34.10 -
   34.11  time_use_thy "UNITY";
   34.12  time_use_thy "Deadlock";
   34.13  time_use_thy "WFair";
   34.14 @@ -32,7 +28,5 @@
   34.15  
   34.16  time_use_thy "ELT";  (*obsolete*)
   34.17  
   34.18 -add_path "../Auth";	(*to find Public.thy*)
   34.19 -use_thy"NSP_Bad";
   34.20 -
   34.21 -reset_path ();
   34.22 +with_path "../Auth"  (*to find Public.thy*)
   34.23 +  time_use_thy"NSP_Bad";
    35.1 --- a/src/HOL/UNITY/UNITY.ML	Tue May 30 16:03:09 2000 +0200
    35.2 +++ b/src/HOL/UNITY/UNITY.ML	Tue May 30 16:08:38 2000 +0200
    35.3 @@ -8,7 +8,7 @@
    35.4  From Misra, "A Logic for Concurrent Programming", 1994
    35.5  *)
    35.6  
    35.7 -set proof_timing;
    35.8 +set timing;
    35.9  
   35.10  (*Perhaps equalities.ML shouldn't add this in the first place!*)
   35.11  Delsimps [image_Collect];
    36.1 --- a/src/HOL/W0/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    36.2 +++ b/src/HOL/W0/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    36.3 @@ -6,8 +6,6 @@
    36.4  Type inference for let-free MiniML
    36.5  *)
    36.6  
    36.7 -writeln"Root file for HOL/W0";
    36.8 -
    36.9  Unify.trace_bound := 20;
   36.10  
   36.11  AddSEs [less_SucE];
    37.1 --- a/src/HOL/ex/BinEx.ML	Tue May 30 16:03:09 2000 +0200
    37.2 +++ b/src/HOL/ex/BinEx.ML	Tue May 30 16:08:38 2000 +0200
    37.3 @@ -9,8 +9,6 @@
    37.4  yields normalized results. 
    37.5  *)
    37.6  
    37.7 -set proof_timing;
    37.8 -
    37.9  (**** The Integers ****)
   37.10  
   37.11  (*** Addition ***)
   37.12 @@ -372,4 +370,3 @@
   37.13  by (safe_tac (claset() addSDs [normal_BIT_D]));
   37.14  by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
   37.15  qed_spec_mp "bin_mult_normal";
   37.16 -
    38.1 --- a/src/HOL/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    38.2 +++ b/src/HOL/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    38.3 @@ -1,4 +1,4 @@
    38.4 -(*  Title:      HOL/ex/ROOT
    38.5 +(*  Title:      HOL/ex/ROOT.ML
    38.6      ID:         $Id$
    38.7      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
    38.8      Copyright   1991  University of Cambridge
    38.9 @@ -6,15 +6,11 @@
   38.10  Executes miscellaneous examples for Higher-Order Logic. 
   38.11  *)
   38.12  
   38.13 -writeln "Root file for HOL examples";
   38.14 -
   38.15 -set proof_timing;
   38.16 -
   38.17  (*some examples of recursive function definitions: the TFL package*)
   38.18  time_use_thy "Recdefs";
   38.19  time_use_thy "Primes";
   38.20  time_use_thy "Fib";
   38.21 -with_path "../Induct" use_thy "Factorization";
   38.22 +with_path "../Induct" time_use_thy "Factorization";
   38.23  time_use_thy "Primrec";
   38.24  
   38.25  time_use_thy "NatSum";
   38.26 @@ -50,6 +46,3 @@
   38.27  (*expressions with quote / antiquote syntax*)
   38.28  time_use_thy "Antiquote";
   38.29  time_use_thy "Multiquote";
   38.30 -
   38.31 -
   38.32 -writeln "END: Root file for HOL examples";
    39.1 --- a/src/HOL/ex/mesontest2.ML	Tue May 30 16:03:09 2000 +0200
    39.2 +++ b/src/HOL/ex/mesontest2.ML	Tue May 30 16:08:38 2000 +0200
    39.3 @@ -19,7 +19,7 @@
    39.4  
    39.5  val meson_tac = safe_meson_tac 1;
    39.6  
    39.7 -set proof_timing;
    39.8 +set timing;
    39.9  
   39.10  (* ========================================================================= *)
   39.11  (* 100 problems selected from the TPTP library                               *)
    40.1 --- a/src/HOLCF/IMP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    40.2 +++ b/src/HOLCF/IMP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    40.3 @@ -4,5 +4,4 @@
    40.4      Copyright   1997  TU Muenchen
    40.5  *)
    40.6  
    40.7 -use_thy "../../HOL/IMP/Natural";
    40.8 -use_thy "HoareEx";
    40.9 +with_path "../../HOL/IMP" time_use_thy "HoareEx";
    41.1 --- a/src/HOLCF/IOA/ABP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    41.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    41.3 @@ -9,4 +9,4 @@
    41.4  
    41.5  goals_limit := 1;
    41.6  
    41.7 -use_thy "Correctness";
    41.8 +time_use_thy "Correctness";
    42.1 --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    42.2 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    42.3 @@ -8,9 +8,8 @@
    42.4  goals_limit := 1;
    42.5  
    42.6  use "../../../HOL/Modelcheck/mucke_oracle.ML";
    42.7 -use_thy "../../../HOL/Modelcheck/MuckeSyn";
    42.8 -use_thy "MuIOAOracle";
    42.9 +with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle";
   42.10  
   42.11  (*examples*)
   42.12 -if_mucke_enabled use_thy "Cockpit";
   42.13 -if_mucke_enabled use_thy "Ring3";
   42.14 +if_mucke_enabled time_use_thy "Cockpit";
   42.15 +if_mucke_enabled time_use_thy "Ring3";
    43.1 --- a/src/HOLCF/IOA/NTP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    43.2 +++ b/src/HOLCF/IOA/NTP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    43.3 @@ -9,4 +9,4 @@
    43.4  
    43.5  goals_limit := 1;
    43.6  
    43.7 -use_thy "Correctness";
    43.8 +time_use_thy "Correctness";
    44.1 --- a/src/HOLCF/IOA/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    44.2 +++ b/src/HOLCF/IOA/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    44.3 @@ -9,6 +9,6 @@
    44.4  
    44.5  goals_limit := 1;
    44.6  
    44.7 -use_thy "meta_theory/Abstraction";
    44.8 -use "meta_theory/ioa_package.ML";
    44.9 -use "meta_theory/ioa_syn.ML";
   44.10 +time_use_thy "meta_theory/Abstraction";
   44.11 +time_use "meta_theory/ioa_package.ML";
   44.12 +time_use "meta_theory/ioa_syn.ML";
    45.1 --- a/src/HOLCF/IOA/Storage/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    45.2 +++ b/src/HOLCF/IOA/Storage/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    45.3 @@ -8,4 +8,4 @@
    45.4  
    45.5  goals_limit := 1;
    45.6  
    45.7 -use_thy "Correctness";
    45.8 +time_use_thy "Correctness";
    46.1 --- a/src/HOLCF/IOA/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    46.2 +++ b/src/HOLCF/IOA/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    46.3 @@ -9,6 +9,5 @@
    46.4  
    46.5  goals_limit := 1;
    46.6  
    46.7 -
    46.8 -use_thy "TrivEx";
    46.9 -use_thy "TrivEx2";
   46.10 +time_use_thy "TrivEx";
   46.11 +time_use_thy "TrivEx2";
    47.1 --- a/src/HOLCF/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    47.2 +++ b/src/HOLCF/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    47.3 @@ -1,14 +1,11 @@
    47.4 -(*  Title:      HOLCF/ex/ROOT
    47.5 +(*  Title:      HOLCF/ex/ROOT.ML
    47.6      ID:         $Id$
    47.7      Author:     Tobias Nipkow
    47.8      Copyright   1994 TU Muenchen
    47.9  
   47.10 -Executes all examples for HOLCF. 
   47.11 +Misc HOLCF examples.
   47.12  *)
   47.13  
   47.14 -writeln"Root file for HOLCF examples";
   47.15 -
   47.16 -set proof_timing;
   47.17  time_use_thy "Dnat";
   47.18  time_use_thy "Stream";
   47.19  time_use_thy "Dagstuhl";
    48.1 --- a/src/LCF/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    48.2 +++ b/src/LCF/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    48.3 @@ -1,9 +1,9 @@
    48.4 -(*  Title:      LCF/ROOT
    48.5 +(*  Title:      LCF/ROOT.ML
    48.6      ID:         $Id$
    48.7      Author:     Tobias Nipkow
    48.8      Copyright   1992  University of Cambridge
    48.9  
   48.10 -Adds LCF to a database containing First-Order Logic.
   48.11 +LCF on top of First-Order Logic.
   48.12  
   48.13  This theory is based on Lawrence Paulson's book Logic and Computation.
   48.14  *)
    49.1 --- a/src/LCF/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    49.2 +++ b/src/LCF/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    49.3 @@ -6,10 +6,7 @@
    49.4  Some examples from Lawrence Paulson's book Logic and Computation.
    49.5  *)
    49.6  
    49.7 -writeln"Root file for LCF examples";
    49.8 -
    49.9 -set proof_timing;
   49.10 -use_thy "Ex1";
   49.11 -use_thy "Ex2";
   49.12 -use_thy "Ex3";
   49.13 -use_thy "Ex4";
   49.14 +time_use_thy "Ex1";
   49.15 +time_use_thy "Ex2";
   49.16 +time_use_thy "Ex3";
   49.17 +time_use_thy "Ex4";
    50.1 --- a/src/Sequents/ILL/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    50.2 +++ b/src/Sequents/ILL/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    50.3 @@ -1,9 +1,4 @@
    50.4 -
    50.5 -writeln"Root file for ILL examples";
    50.6 -
    50.7 -set proof_timing;
    50.8  
    50.9  time_use_thy "washing";
   50.10 -
   50.11  time_use_thy "ILL_predlog";
   50.12  time_use "ILL_kleene_lemmas.ML";
    51.1 --- a/src/Sequents/LK/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    51.2 +++ b/src/Sequents/LK/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    51.3 @@ -1,4 +1,4 @@
    51.4 -(*  Title:      LK/ex/ROOT
    51.5 +(*  Title:      LK/ex/ROOT.ML
    51.6      ID:         $Id$
    51.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    51.8      Copyright   1992  University of Cambridge
    51.9 @@ -6,10 +6,7 @@
   51.10  Executes all examples for Classical Logic. 
   51.11  *)
   51.12  
   51.13 -writeln"Root file for LK examples";
   51.14 -
   51.15 -set proof_timing;
   51.16  time_use "prop.ML";
   51.17  time_use "quant.ML";
   51.18  time_use "hardquant.ML";
   51.19 -use_thy "Nat";
   51.20 +time_use_thy "Nat";
    52.1 --- a/src/Sequents/Modal/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    52.2 +++ b/src/Sequents/Modal/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    52.3 @@ -4,8 +4,6 @@
    52.4      Copyright   1991  University of Cambridge
    52.5  *)
    52.6  
    52.7 -set proof_timing;
    52.8 -
    52.9  writeln "\nTheorems of T\n";
   52.10  fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
   52.11  time_use "Tthms.ML";
    53.1 --- a/src/Sequents/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    53.2 +++ b/src/Sequents/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    53.3 @@ -1,4 +1,4 @@
    53.4 -(*  Title:      Sequents/ROOT
    53.5 +(*  Title:      Sequents/ROOT.ML
    53.6      ID:         $Id$
    53.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    53.8      Copyright   1991  University of Cambridge
    54.1 --- a/src/ZF/AC/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    54.2 +++ b/src/ZF/AC/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    54.3 @@ -6,9 +6,6 @@
    54.4  Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
    54.5  *)
    54.6  
    54.7 -writeln"Root file for ZF/AC";
    54.8 -set proof_timing;
    54.9 -
   54.10  time_use_thy "AC_Equiv";
   54.11  
   54.12  time_use     "WO1_WO6.ML";
   54.13 @@ -35,5 +32,3 @@
   54.14  time_use_thy "AC18_AC19";
   54.15  
   54.16  time_use_thy "DC";
   54.17 -
   54.18 -writeln"END: Root file for ZF/AC";
    55.1 --- a/src/ZF/Coind/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    55.2 +++ b/src/ZF/Coind/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    55.3 @@ -13,7 +13,4 @@
    55.4      Report, Computer Lab, University of Cambridge (1995).
    55.5  *)
    55.6  
    55.7 -writeln"Root file for ZF/Coind";
    55.8 -
    55.9 -set proof_timing;
   55.10  time_use_thy "MT";
    56.1 --- a/src/ZF/Datatype.ML	Tue May 30 16:03:09 2000 +0200
    56.2 +++ b/src/ZF/Datatype.ML	Tue May 30 16:08:38 2000 +0200
    56.3 @@ -53,7 +53,7 @@
    56.4  structure DataFree =
    56.5  struct
    56.6    (*prove while suppressing timing information*)
    56.7 -  fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
    56.8 +  fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
    56.9  
   56.10    val trace = ref false;
   56.11  
    57.1 --- a/src/ZF/IMP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    57.2 +++ b/src/ZF/IMP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    57.3 @@ -12,7 +12,4 @@
    57.4  
    57.5  *)
    57.6  
    57.7 -writeln"Root file for ZF/IMP";
    57.8 -
    57.9 -set proof_timing;
   57.10  time_use_thy "Equiv";
    58.1 --- a/src/ZF/Resid/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    58.2 +++ b/src/ZF/Resid/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    58.3 @@ -12,9 +12,4 @@
    58.4  J. Functional Programming 4(3) 1994, 371-394.
    58.5  *)
    58.6  
    58.7 -writeln"Root file for ZF/Resid";
    58.8 -
    58.9 -set proof_timing;
   58.10  time_use_thy "Conversion";
   58.11 -
   58.12 -writeln"END: Root file for ZF/Resid";
    59.1 --- a/src/ZF/ex/BinEx.ML	Tue May 30 16:03:09 2000 +0200
    59.2 +++ b/src/ZF/ex/BinEx.ML	Tue May 30 16:08:38 2000 +0200
    59.3 @@ -8,7 +8,6 @@
    59.4  
    59.5  context Bin.thy;
    59.6  
    59.7 -set proof_timing;
    59.8  (*All runtimes below are on a 300MHz Pentium*)
    59.9  
   59.10  Goal "#13  $+  #19 = #32";
    60.1 --- a/src/ZF/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
    60.2 +++ b/src/ZF/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
    60.3 @@ -6,9 +6,6 @@
    60.4  Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
    60.5  *)
    60.6  
    60.7 -writeln"Root file for ZF Set Theory examples";
    60.8 -set proof_timing;
    60.9 -
   60.10  time_use     "misc.ML";
   60.11  time_use_thy "Primes";          (*GCD theory*)
   60.12  time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
   60.13 @@ -37,5 +34,3 @@
   60.14  (** CoDatatypes **)
   60.15  time_use_thy "LList";
   60.16  time_use_thy "CoUnit";
   60.17 -
   60.18 -writeln"END: Root file for ZF Set Theory examples";