# HG changeset patch
# User wenzelm
# Date 959695718 -7200
# Node ID c20d58286a51a4a787a7728e64336df2eb559438
# Parent  ad8260dc6e4a0a6c622be477da1d93f04f25c976
cleaned up;

diff -r ad8260dc6e4a -r c20d58286a51 Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,7 +6,7 @@
 
 val tests = ["Brackin", "Instructions", "SML", "Verilog"];
 
-set Toplevel.trace;
+set timing;
 
 warning "\nset quick_and_dirty\n"; set quick_and_dirty;
 seq time_use_thy tests;
diff -r ad8260dc6e4a -r c20d58286a51 src/CCL/ROOT.ML
--- a/src/CCL/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/CCL/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      CCL/ROOT
+(*  Title:      CCL/ROOT.ML
     ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
diff -r ad8260dc6e4a -r c20d58286a51 src/CCL/ex/ROOT.ML
--- a/src/CCL/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/CCL/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      CCL/ex/ROOT
+(*  Title:      CCL/ex/ROOT.ML
     ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -6,9 +6,6 @@
 Executes all examples for Classical Computational Logic
 *)
 
-writeln"Root file for CCL examples";
-set proof_timing;
-
 time_use_thy "Nat";
 time_use_thy "List";
 time_use_thy "Stream";
diff -r ad8260dc6e4a -r c20d58286a51 src/CTT/ex/ROOT.ML
--- a/src/CTT/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/CTT/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      CTT/ex/ROOT
+(*  Title:      CTT/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -6,10 +6,7 @@
 Executes all examples for Constructive Type Theory. 
 *)
 
-writeln"Root file for CTT examples";
-
 print_depth 2;  
-set proof_timing;
 
 time_use "typechk.ML";
 time_use "elim.ML";
diff -r ad8260dc6e4a -r c20d58286a51 src/Cube/ex/ROOT.ML
--- a/src/Cube/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/Cube/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,5 +1,2 @@
 
-writeln"Root file for Cube examples";
-
-set proof_timing;
-use_thy "ex";
+time_use_thy "ex";
diff -r ad8260dc6e4a -r c20d58286a51 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/FOL/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,10 +6,6 @@
 Executes all examples for First-Order Logic. 
 *)
 
-writeln"Root file for FOL examples";
-
-set proof_timing;
-
 time_use     "intro.ML";
 time_use_thy "Nat";
 time_use     "foundn.ML";
diff -r ad8260dc6e4a -r c20d58286a51 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/FOLP/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,10 +6,6 @@
 Executes all examples for First-Order Logic. 
 *)
 
-writeln"Root file for FOLP examples";
-
-set proof_timing;
-
 time_use     "intro.ML";
 time_use_thy "Nat";
 time_use     "foundn.ML";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,5 +4,5 @@
     Author: Clemens Ballarin, started 24 September 1999
 *)
 
-with_path "abstract" use_thy "Abstract";        (*The ring theory*)
-with_path "poly"     use_thy "Polynomial";      (*The full theory*)
+with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
+with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Tue May 30 16:08:38 2000 +0200
@@ -7,7 +7,7 @@
 *)
 
 Pretty.setdepth 20;
-proof_timing:=true;
+set timing;
 
 AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
 
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Auth/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,9 +6,6 @@
 Root file for protocol proofs.
 *)
 
-writeln"Root file for HOL/Auth";
-
-set proof_timing;
 goals_limit := 1;
 
 (*Shared-key protocols*)
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/AxClasses/Group/ROOT.ML
--- a/src/HOL/AxClasses/Group/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/AxClasses/Group/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,7 +8,7 @@
 set show_types;
 set show_sorts;
 
-use_thy "Monoid";
-use_thy "Group";
-use_thy "MonoidGroupInsts";
-use_thy "GroupInsts";
+time_use_thy "Monoid";
+time_use_thy "Group";
+time_use_thy "MonoidGroupInsts";
+time_use_thy "GroupInsts";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/AxClasses/Lattice/ROOT.ML
--- a/src/HOL/AxClasses/Lattice/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/AxClasses/Lattice/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -11,14 +11,14 @@
 set show_types;
 set show_sorts;
 
-use_thy "Order";
-use_thy "OrdDefs";
-use_thy "OrdInsts";
+time_use_thy "Order";
+time_use_thy "OrdDefs";
+time_use_thy "OrdInsts";
 
-use_thy "Lattice";
-use_thy "CLattice";
+time_use_thy "Lattice";
+time_use_thy "CLattice";
 
-use_thy "LatPreInsts";
-use_thy "LatInsts";
+time_use_thy "LatPreInsts";
+time_use_thy "LatInsts";
 
-use_thy "LatMorph";
+time_use_thy "LatMorph";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/AxClasses/Tutorial/ROOT.ML
--- a/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
 
-use_thy "Semigroups";
-use_thy "Group";
-use_thy "Product";
+time_use_thy "Semigroups";
+time_use_thy "Group";
+time_use_thy "Product";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/BCV/ROOT.ML
--- a/src/HOL/BCV/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/BCV/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -7,6 +7,4 @@
 aka `bytecode verification'.
 *)
 
-writeln"Root file for HOL/BCV";
-
 time_use_thy "Machine";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Hoare/ROOT.ML
--- a/src/HOL/Hoare/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Hoare/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,4 +4,4 @@
     Copyright   1998 TUM
 *)
 
-use_thy "Examples";
+time_use_thy "Examples";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/IMP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,9 +4,6 @@
     Copyright   1995 TUM
 *)
 
-writeln"Root file for HOL/IMP";
-
-set proof_timing;
 time_use_thy "Expr";
 time_use_thy "Transition";
 time_use_thy "VC";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/IMPP/ROOT.ML
--- a/src/HOL/IMPP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/IMPP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,6 +4,4 @@
     Copyright   1999 TUM
 *)
 
-writeln"Root file for HOL/IMPP";
-
-use_thy "EvenOdd";
+time_use_thy "EvenOdd";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Induct/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,9 +6,6 @@
 Examples of Inductive and Coinductive Definitions
 *)
 
-writeln"Root file for HOL/Induct";
-
-set proof_timing;
 time_use_thy "Perm";
 time_use_thy "Comb";
 time_use_thy "Mutil";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Tue May 30 16:08:38 2000 +0200
@@ -308,7 +308,7 @@
 
 (*examples:
 print_depth 22;
-set proof_timing;
+set timing;
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Tue May 30 16:08:38 2000 +0200
@@ -287,7 +287,7 @@
 
 (*examples:
 print_depth 22;
-set proof_timing;
+set timing;
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,8 +4,6 @@
     Copyright   1998 TUM
 *)
 
-writeln"Root file for HOL/Lambda";
-
 time_use_thy "Eta";
-time_use_thy "../Induct/Acc";
+with_path "../Induct" time_use_thy "Acc";
 time_use_thy "InductTermi";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Lex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,8 +4,8 @@
     Copyright   1998 TUM
 *)
 
-use_thy"AutoChopper";
-use_thy"AutoChopper1";
-use_thy"AutoMaxChop";
-use_thy"RegSet_of_nat_DA";
-use_thy"Scanner";
+time_use_thy "AutoChopper";
+time_use_thy "AutoChopper1";
+time_use_thy "AutoMaxChop";
+time_use_thy "RegSet_of_nat_DA";
+time_use_thy "Scanner";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/MicroJava/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,12 +1,8 @@
+
 goals_limit:=1;
 
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 
-add_path "J";
-add_path "JVM";
-add_path "BV";
-
-
-use_thy "JTypeSafe";
-use_thy "BVSpecTypeSafe";
+with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "JTypeSafe";
+with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "BVSpecTypeSafe";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/MiniML/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,6 +6,4 @@
 Type inference for MiniML
 *)
 
-writeln"Root file for HOL/MiniML";
-
 time_use_thy "W";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Modelcheck/ROOT.ML
--- a/src/HOL/Modelcheck/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,16 +8,16 @@
 
 (* Mucke -- mu-calculus model checker from Karlsruhe *)
 
-use "mucke_oracle.ML";
-use_thy "MuckeSyn";
+time_use "mucke_oracle.ML";
+time_use_thy "MuckeSyn";
 
-if_mucke_enabled use_thy "MuckeExample1";
-if_mucke_enabled use_thy "MuckeExample2";
+if_mucke_enabled time_use_thy "MuckeExample1";
+if_mucke_enabled time_use_thy "MuckeExample2";
 
 
 (* Einhoven model checker *)
 
-use_thy "CTL";
-use_thy "EindhovenSyn";
+time_use_thy "CTL";
+time_use_thy "EindhovenSyn";
 
-if_eindhoven_enabled use_thy "EindhovenExample";
+if_eindhoven_enabled time_use_thy "EindhovenExample";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Quot/ROOT.ML
--- a/src/HOL/Quot/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Quot/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,11 +1,7 @@
 (*  Title:      HOL/Quot/ROOT.ML
     ID:         $Id$
-    Author:     
-    Copyright   
 
 Higher-order quotients.
 *)
 
-writeln"Root file for HOL/Quot";
-
-use_thy "FRACT";
+time_use_thy "FRACT";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Real/ROOT.ML
--- a/src/HOL/Real/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Real/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,8 +8,6 @@
 Linear real arithmetic is installed in RealBin.ML.
 *)
 
-writeln"Root file for HOL/Real";
-
 time_use_thy "RealDef";
 use          "simproc.ML";
 time_use_thy "Real";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Real/ex/ROOT.ML
--- a/src/HOL/Real/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Real/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,8 +6,4 @@
 HOL/Real examples.
 *)
 
-writeln "Root file for HOL/Real examples";
-
-set proof_timing;
-
 time_use_thy "BinEx";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Subst/ROOT.ML
--- a/src/HOL/Subst/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/Subst/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -22,12 +22,6 @@
                 correctness and termination
 Unify        -  the unification function
 
-To load, type use"ROOT.ML"; into an Isabelle-HOL that has TFL 
-also loaded. 
 *)
 
-writeln"Root file for Substitutions and Unification";
-
-use_thy "Unify";
-
-writeln"END: Root file for Substitutions and Unification";
+time_use_thy "Unify";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/TLA/Buffer/ROOT.ML
--- a/src/HOL/TLA/Buffer/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/TLA/Buffer/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,2 +1,2 @@
 
-use_thy "DBuffer";
+time_use_thy "DBuffer";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/TLA/Inc/ROOT.ML
--- a/src/HOL/TLA/Inc/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/TLA/Inc/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,2 +1,2 @@
 
-use_thy "Inc";
+time_use_thy "Inc";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/TLA/Memory/ROOT.ML
--- a/src/HOL/TLA/Memory/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/TLA/Memory/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,2 +1,2 @@
 
-use_thy "MemoryImplementation";
+time_use_thy "MemoryImplementation";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/TLA/ROOT.ML
--- a/src/HOL/TLA/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/TLA/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -5,4 +5,4 @@
 
 val banner = "Temporal Logic of Actions";
 
-use_thy "TLA";
+time_use_thy "TLA";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,10 +6,6 @@
 Root file for UNITY proofs.
 *)
 
-writeln"Root file for HOL/UNITY";
-
-set proof_timing;
-
 time_use_thy "UNITY";
 time_use_thy "Deadlock";
 time_use_thy "WFair";
@@ -32,7 +28,5 @@
 
 time_use_thy "ELT";  (*obsolete*)
 
-add_path "../Auth";	(*to find Public.thy*)
-use_thy"NSP_Bad";
-
-reset_path ();
+with_path "../Auth"  (*to find Public.thy*)
+  time_use_thy"NSP_Bad";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,7 +8,7 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-set proof_timing;
+set timing;
 
 (*Perhaps equalities.ML shouldn't add this in the first place!*)
 Delsimps [image_Collect];
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/W0/ROOT.ML
--- a/src/HOL/W0/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/W0/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,8 +6,6 @@
 Type inference for let-free MiniML
 *)
 
-writeln"Root file for HOL/W0";
-
 Unify.trace_bound := 20;
 
 AddSEs [less_SucE];
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/ex/BinEx.ML
--- a/src/HOL/ex/BinEx.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/ex/BinEx.ML	Tue May 30 16:08:38 2000 +0200
@@ -9,8 +9,6 @@
 yields normalized results. 
 *)
 
-set proof_timing;
-
 (**** The Integers ****)
 
 (*** Addition ***)
@@ -372,4 +370,3 @@
 by (safe_tac (claset() addSDs [normal_BIT_D]));
 by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
 qed_spec_mp "bin_mult_normal";
-
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/ROOT
+(*  Title:      HOL/ex/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -6,15 +6,11 @@
 Executes miscellaneous examples for Higher-Order Logic. 
 *)
 
-writeln "Root file for HOL examples";
-
-set proof_timing;
-
 (*some examples of recursive function definitions: the TFL package*)
 time_use_thy "Recdefs";
 time_use_thy "Primes";
 time_use_thy "Fib";
-with_path "../Induct" use_thy "Factorization";
+with_path "../Induct" time_use_thy "Factorization";
 time_use_thy "Primrec";
 
 time_use_thy "NatSum";
@@ -50,6 +46,3 @@
 (*expressions with quote / antiquote syntax*)
 time_use_thy "Antiquote";
 time_use_thy "Multiquote";
-
-
-writeln "END: Root file for HOL examples";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOL/ex/mesontest2.ML	Tue May 30 16:08:38 2000 +0200
@@ -19,7 +19,7 @@
 
 val meson_tac = safe_meson_tac 1;
 
-set proof_timing;
+set timing;
 
 (* ========================================================================= *)
 (* 100 problems selected from the TPTP library                               *)
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IMP/ROOT.ML
--- a/src/HOLCF/IMP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IMP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,5 +4,4 @@
     Copyright   1997  TU Muenchen
 *)
 
-use_thy "../../HOL/IMP/Natural";
-use_thy "HoareEx";
+with_path "../../HOL/IMP" time_use_thy "HoareEx";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IOA/ABP/ROOT.ML
--- a/src/HOLCF/IOA/ABP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IOA/ABP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -9,4 +9,4 @@
 
 goals_limit := 1;
 
-use_thy "Correctness";
+time_use_thy "Correctness";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IOA/Modelcheck/ROOT.ML
--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,9 +8,8 @@
 goals_limit := 1;
 
 use "../../../HOL/Modelcheck/mucke_oracle.ML";
-use_thy "../../../HOL/Modelcheck/MuckeSyn";
-use_thy "MuIOAOracle";
+with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle";
 
 (*examples*)
-if_mucke_enabled use_thy "Cockpit";
-if_mucke_enabled use_thy "Ring3";
+if_mucke_enabled time_use_thy "Cockpit";
+if_mucke_enabled time_use_thy "Ring3";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IOA/NTP/ROOT.ML
--- a/src/HOLCF/IOA/NTP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IOA/NTP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -9,4 +9,4 @@
 
 goals_limit := 1;
 
-use_thy "Correctness";
+time_use_thy "Correctness";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -9,6 +9,6 @@
 
 goals_limit := 1;
 
-use_thy "meta_theory/Abstraction";
-use "meta_theory/ioa_package.ML";
-use "meta_theory/ioa_syn.ML";
+time_use_thy "meta_theory/Abstraction";
+time_use "meta_theory/ioa_package.ML";
+time_use "meta_theory/ioa_syn.ML";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IOA/Storage/ROOT.ML
--- a/src/HOLCF/IOA/Storage/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IOA/Storage/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,4 +8,4 @@
 
 goals_limit := 1;
 
-use_thy "Correctness";
+time_use_thy "Correctness";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/IOA/ex/ROOT.ML
--- a/src/HOLCF/IOA/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IOA/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -9,6 +9,5 @@
 
 goals_limit := 1;
 
-
-use_thy "TrivEx";
-use_thy "TrivEx2";
+time_use_thy "TrivEx";
+time_use_thy "TrivEx2";
diff -r ad8260dc6e4a -r c20d58286a51 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,14 +1,11 @@
-(*  Title:      HOLCF/ex/ROOT
+(*  Title:      HOLCF/ex/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
-Executes all examples for HOLCF. 
+Misc 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 ad8260dc6e4a -r c20d58286a51 src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/LCF/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,9 +1,9 @@
-(*  Title:      LCF/ROOT
+(*  Title:      LCF/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
-Adds LCF to a database containing First-Order Logic.
+LCF on top of First-Order Logic.
 
 This theory is based on Lawrence Paulson's book Logic and Computation.
 *)
diff -r ad8260dc6e4a -r c20d58286a51 src/LCF/ex/ROOT.ML
--- a/src/LCF/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/LCF/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,10 +6,7 @@
 Some examples from Lawrence Paulson's book Logic and Computation.
 *)
 
-writeln"Root file for LCF examples";
-
-set proof_timing;
-use_thy "Ex1";
-use_thy "Ex2";
-use_thy "Ex3";
-use_thy "Ex4";
+time_use_thy "Ex1";
+time_use_thy "Ex2";
+time_use_thy "Ex3";
+time_use_thy "Ex4";
diff -r ad8260dc6e4a -r c20d58286a51 src/Sequents/ILL/ROOT.ML
--- a/src/Sequents/ILL/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/Sequents/ILL/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,9 +1,4 @@
-
-writeln"Root file for ILL examples";
-
-set proof_timing;
 
 time_use_thy "washing";
-
 time_use_thy "ILL_predlog";
 time_use "ILL_kleene_lemmas.ML";
diff -r ad8260dc6e4a -r c20d58286a51 src/Sequents/LK/ROOT.ML
--- a/src/Sequents/LK/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/Sequents/LK/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/ex/ROOT
+(*  Title:      LK/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -6,10 +6,7 @@
 Executes all examples for Classical Logic. 
 *)
 
-writeln"Root file for LK examples";
-
-set proof_timing;
 time_use "prop.ML";
 time_use "quant.ML";
 time_use "hardquant.ML";
-use_thy "Nat";
+time_use_thy "Nat";
diff -r ad8260dc6e4a -r c20d58286a51 src/Sequents/Modal/ROOT.ML
--- a/src/Sequents/Modal/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/Sequents/Modal/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -4,8 +4,6 @@
     Copyright   1991  University of Cambridge
 *)
 
-set proof_timing;
-
 writeln "\nTheorems of T\n";
 fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
 time_use "Tthms.ML";
diff -r ad8260dc6e4a -r c20d58286a51 src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/Sequents/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Sequents/ROOT
+(*  Title:      Sequents/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/AC/ROOT.ML
--- a/src/ZF/AC/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/AC/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,9 +6,6 @@
 Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
 *)
 
-writeln"Root file for ZF/AC";
-set proof_timing;
-
 time_use_thy "AC_Equiv";
 
 time_use     "WO1_WO6.ML";
@@ -35,5 +32,3 @@
 time_use_thy "AC18_AC19";
 
 time_use_thy "DC";
-
-writeln"END: Root file for ZF/AC";
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/Coind/ROOT.ML
--- a/src/ZF/Coind/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/Coind/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -13,7 +13,4 @@
     Report, Computer Lab, University of Cambridge (1995).
 *)
 
-writeln"Root file for ZF/Coind";
-
-set proof_timing;
 time_use_thy "MT";
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/Datatype.ML	Tue May 30 16:08:38 2000 +0200
@@ -53,7 +53,7 @@
 structure DataFree =
 struct
   (*prove while suppressing timing information*)
-  fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
+  fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
 
   val trace = ref false;
 
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/IMP/ROOT.ML
--- a/src/ZF/IMP/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/IMP/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -12,7 +12,4 @@
 
 *)
 
-writeln"Root file for ZF/IMP";
-
-set proof_timing;
 time_use_thy "Equiv";
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/Resid/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -12,9 +12,4 @@
 J. Functional Programming 4(3) 1994, 371-394.
 *)
 
-writeln"Root file for ZF/Resid";
-
-set proof_timing;
 time_use_thy "Conversion";
-
-writeln"END: Root file for ZF/Resid";
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/ex/BinEx.ML
--- a/src/ZF/ex/BinEx.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/ex/BinEx.ML	Tue May 30 16:08:38 2000 +0200
@@ -8,7 +8,6 @@
 
 context Bin.thy;
 
-set proof_timing;
 (*All runtimes below are on a 300MHz Pentium*)
 
 Goal "#13  $+  #19 = #32";
diff -r ad8260dc6e4a -r c20d58286a51 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/ZF/ex/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,9 +6,6 @@
 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
 *)
 
-writeln"Root file for ZF Set Theory examples";
-set proof_timing;
-
 time_use     "misc.ML";
 time_use_thy "Primes";          (*GCD theory*)
 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
@@ -37,5 +34,3 @@
 (** CoDatatypes **)
 time_use_thy "LList";
 time_use_thy "CoUnit";
-
-writeln"END: Root file for ZF Set Theory examples";