summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 30 May 2000 16:08:38 +0200 | |

changeset 9000 | c20d58286a51 |

parent 8999 | ad8260dc6e4a |

child 9001 | 93af64f54bf2 |

cleaned up;

--- 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";