1.1 --- a/src/HOL/AxClasses/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
1.2 +++ b/src/HOL/AxClasses/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
1.3 @@ -1,4 +1,3 @@
1.4 +(* $Id$ *)
1.5
1.6 -time_use_thy "Semigroups";
1.7 -time_use_thy "Group";
1.8 -time_use_thy "Product";
1.9 +use_thys ["Semigroups", "Group", "Product"];
2.1 --- a/src/HOL/Extraction/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
2.2 +++ b/src/HOL/Extraction/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
2.3 @@ -8,8 +8,5 @@
2.4 warning "HOL proof terms required for running extraction examples"
2.5 else
2.6 (proofs := 2;
2.7 - time_use_thy "QuotRem";
2.8 - time_use_thy "Warshall";
2.9 - time_use_thy "Higman";
2.10 no_document time_use_thy "Efficient_Nat";
2.11 - time_use_thy "Pigeonhole");
2.12 + use_thys ["QuotRem", "Warshall", "Higman", "Pigeonhole"]);
3.1 --- a/src/HOL/Hoare/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
3.2 +++ b/src/HOL/Hoare/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
3.3 @@ -4,10 +4,5 @@
3.4 Copyright 1998-2003 TUM
3.5 *)
3.6
3.7 -time_use_thy "Examples";
3.8 -time_use_thy "ExamplesAbort";
3.9 -time_use_thy "Pointers0";
3.10 -time_use_thy "Pointer_Examples";
3.11 -time_use_thy "Pointer_ExamplesAbort";
3.12 -time_use_thy "SchorrWaite";
3.13 -time_use_thy "Separation";
3.14 +use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples",
3.15 + "Pointer_ExamplesAbort", "SchorrWaite", "Separation"];
4.1 --- a/src/HOL/HoareParallel/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
4.2 +++ b/src/HOL/HoareParallel/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
4.3 @@ -1,5 +1,3 @@
4.4 +(* $Id$ *)
4.5
4.6 -time_use_thy "OG_Examples";
4.7 -time_use_thy "Gar_Coll";
4.8 -time_use_thy "Mul_Gar_Coll";
4.9 -time_use_thy "RG_Examples";
4.10 +use_thys ["OG_Examples", "Gar_Coll", "Mul_Gar_Coll", "RG_Examples"];
5.1 --- a/src/HOL/IMP/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
5.2 +++ b/src/HOL/IMP/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
5.3 @@ -6,9 +6,4 @@
5.4 Caveat: HOLCF/IMP depends on HOL/IMP
5.5 *)
5.6
5.7 -time_use_thy "Expr";
5.8 -time_use_thy "Transition";
5.9 -time_use_thy "VC";
5.10 -time_use_thy "Examples";
5.11 -time_use_thy "Compiler0";
5.12 -time_use_thy "Compiler";
5.13 +use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler"];
6.1 --- a/src/HOL/Induct/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
6.2 +++ b/src/HOL/Induct/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
6.3 @@ -1,16 +1,6 @@
6.4
6.5 (* $Id$ *)
6.6
6.7 -time_use_thy "Mutil";
6.8 -time_use_thy "QuoDataType";
6.9 -time_use_thy "QuoNestedDataType";
6.10 -time_use_thy "Term";
6.11 -time_use_thy "ABexp";
6.12 -time_use_thy "Tree";
6.13 -time_use_thy "Ordinals";
6.14 -time_use_thy "Sigma_Algebra";
6.15 -time_use_thy "Comb";
6.16 -time_use_thy "PropLog";
6.17 -time_use_thy "SList";
6.18 -time_use_thy "LFilter";
6.19 -time_use_thy "Com";
6.20 +use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",
6.21 + "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
6.22 + "SList", "LFilter", "Com"];
7.1 --- a/src/HOL/Lambda/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
7.2 +++ b/src/HOL/Lambda/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
7.3 @@ -7,9 +7,8 @@
7.4 Syntax.ambiguity_level := 100;
7.5 proofs := 2;
7.6
7.7 -use_thy "Eta";
7.8 no_document use_thy "Accessible_Part";
7.9 -use_thy "StrongNorm";
7.10 +use_thys ["Eta", "StrongNorm"];
7.11 if HOL_proofs < 2 then
7.12 warning "HOL proof terms required for running theory WeakNorm"
7.13 else use_thy "WeakNorm";
8.1 --- a/src/HOL/Library/Library/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
8.2 +++ b/src/HOL/Library/Library/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
8.3 @@ -1,6 +1,3 @@
8.4 (* $Id$ *)
8.5
8.6 -use_thy "Library";
8.7 -use_thy "List_Prefix";
8.8 -use_thy "List_lexord";
8.9 -use_thy "SCT_Examples";
8.10 +use_thys ["Library", "List_Prefix", "List_lexord", "SCT_Examples"];
9.1 --- a/src/HOL/NumberTheory/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
9.2 +++ b/src/HOL/NumberTheory/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
9.3 @@ -1,12 +1,5 @@
9.4 (* $Id$ *)
9.5
9.6 -no_document use_thy "Infinite_Set";
9.7 -no_document use_thy "Permutation";
9.8 -no_document use_thy "Primes";
9.9 -
9.10 -use_thy "Fib";
9.11 -use_thy "Factorization";
9.12 -use_thy "Chinese";
9.13 -use_thy "WilsonRuss";
9.14 -use_thy "WilsonBij";
9.15 -use_thy "Quadratic_Reciprocity";
9.16 +no_document use_thys ["Infinite_Set", "Permutation", "Primes"];
9.17 +use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
9.18 + "WilsonBij", "Quadratic_Reciprocity"];
10.1 --- a/src/HOL/Prolog/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
10.2 +++ b/src/HOL/Prolog/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
10.3 @@ -3,5 +3,4 @@
10.4 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
10.5 *)
10.6
10.7 -use_thy"Test";
10.8 -use_thy"Type";
10.9 \ No newline at end of file
10.10 +use_thys ["Test", "Type"];
11.1 --- a/src/HOL/SET-Protocol/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
11.2 +++ b/src/HOL/SET-Protocol/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
11.3 @@ -1,4 +1,4 @@
11.4 -(* Title: HOL/SET-Protocol/ROOT
11.5 +(* Title: HOL/SET-Protocol/ROOT.ML
11.6 ID: $Id$
11.7 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
11.8 Copyright 2003 University of Cambridge
11.9 @@ -6,11 +6,5 @@
11.10 Root file for the SET protocol proofs.
11.11 *)
11.12
11.13 -goals_limit := 1;
11.14 -set timing;
11.15 -
11.16 no_document use_thy "NatPair";
11.17 -time_use_thy "Cardholder_Registration";
11.18 -time_use_thy "Merchant_Registration";
11.19 -time_use_thy "Purchase";
11.20 -
11.21 +use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];