simultaneous use_thys;
authorwenzelm
Tue Jul 31 22:21:20 2007 +0200 (2007-07-31)
changeset 24104719fbe4fb77f
parent 24103 c13243a11e37
child 24105 af364e2b4048
simultaneous use_thys;
src/HOL/AxClasses/ROOT.ML
src/HOL/Extraction/ROOT.ML
src/HOL/Hoare/ROOT.ML
src/HOL/HoareParallel/ROOT.ML
src/HOL/IMP/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/Lambda/ROOT.ML
src/HOL/Library/Library/ROOT.ML
src/HOL/NumberTheory/ROOT.ML
src/HOL/Prolog/ROOT.ML
src/HOL/SET-Protocol/ROOT.ML
     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"];