--- 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;
--- 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
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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*)
--- 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];
--- 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*)
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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));
--- 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));
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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];
--- 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];
--- 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";
-
--- 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";
--- 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 *)
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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.
*)
--- 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";
--- 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";
--- 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";
--- 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";
--- 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
--- 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";
--- 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";
--- 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;
--- 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";
--- 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";
--- 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";
--- 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";