uniform use of simultabeous use_thys;
authorwenzelm
Wed Nov 11 14:15:11 2009 +0100 (2009-11-11)
changeset 33615261abc2e3155
parent 33608 5c0024338cef
child 33616 69f0a6271825
uniform use of simultabeous use_thys;
src/CTT/ROOT.ML
src/FOL/ROOT.ML
src/FOLP/ROOT.ML
src/HOL/Bali/ROOT.ML
src/HOL/Boogie/ROOT.ML
src/HOL/Decision_Procs/ROOT.ML
src/HOL/Hahn_Banach/ROOT.ML
src/HOL/Hoare_Parallel/ROOT.ML
src/HOL/IMPP/ROOT.ML
src/HOL/IOA/ROOT.ML
src/HOL/Imperative_HOL/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/Lambda/ROOT.ML
src/HOL/Lattice/ROOT.ML
src/HOL/MicroJava/ROOT.ML
src/HOL/Mirabelle/ROOT.ML
src/HOL/Multivariate_Analysis/ROOT.ML
src/HOL/NSA/Examples/ROOT.ML
src/HOL/NSA/ROOT.ML
src/HOL/NanoJava/ROOT.ML
src/HOL/Nominal/Examples/ROOT.ML
src/HOL/Nominal/ROOT.ML
src/HOL/Number_Theory/ROOT.ML
src/HOL/Probability/ROOT.ML
src/HOL/ROOT.ML
src/HOL/SET_Protocol/ROOT.ML
src/HOL/SMT/Examples/ROOT.ML
src/HOL/SMT/ROOT.ML
src/HOL/Statespace/ROOT.ML
src/HOL/Subst/ROOT.ML
src/HOL/TLA/Buffer/ROOT.ML
src/HOL/TLA/Inc/ROOT.ML
src/HOL/TLA/Memory/ROOT.ML
src/HOL/TLA/ROOT.ML
src/HOL/UNITY/ROOT.ML
src/HOL/Unix/ROOT.ML
src/HOL/W0/ROOT.ML
src/HOL/Word/Examples/ROOT.ML
src/HOL/Word/ROOT.ML
src/HOL/ZF/ROOT.ML
src/HOL/base.ML
src/HOL/main.ML
src/HOL/plain.ML
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/NTP/ROOT.ML
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/Storage/ROOT.ML
src/HOLCF/IOA/ex/ROOT.ML
src/HOLCF/ROOT.ML
src/LCF/ROOT.ML
src/ZF/Coind/ROOT.ML
src/ZF/IMP/ROOT.ML
src/ZF/Resid/ROOT.ML
     1.1 --- a/src/CTT/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     1.2 +++ b/src/CTT/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     1.3 @@ -1,8 +1,7 @@
     1.4  (*  Title:      CTT/ROOT.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1991  University of Cambridge
     1.8  *)
     1.9  
    1.10 -use_thy "Main";
    1.11 +use_thys ["Main"];
    1.12  
     2.1 --- a/src/FOL/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     2.3 @@ -1,3 +1,3 @@
     2.4  (* First-Order Logic with Natural Deduction *)
     2.5  
     2.6 -use_thy "FOL";
     2.7 +use_thys ["FOL"];
     3.1 --- a/src/FOLP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     3.2 +++ b/src/FOLP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     3.3 @@ -1,6 +1,5 @@
     3.4  (*  Title:      FOLP/ROOT.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     martin Coen, Cambridge University Computer Laboratory
     3.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     3.8      Copyright   1993  University of Cambridge
     3.9  
    3.10  Modifed version of Lawrence Paulson's FOL that contains proof terms.
    3.11 @@ -8,5 +7,5 @@
    3.12  Presence of unknown proof term means that matching does not behave as expected.
    3.13  *)
    3.14  
    3.15 -use_thy "FOLP";
    3.16 +use_thys ["FOLP"];
    3.17  
     4.1 --- a/src/HOL/Bali/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     4.2 +++ b/src/HOL/Bali/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     4.3 @@ -1,2 +1,1 @@
     4.4 -
     4.5 -use_thy "Bali"
     4.6 +use_thys ["Bali"];
     5.1 --- a/src/HOL/Boogie/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     5.2 +++ b/src/HOL/Boogie/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     5.3 @@ -1,1 +1,1 @@
     5.4 -use_thy "Boogie";
     5.5 +use_thys ["Boogie"];
     6.1 --- a/src/HOL/Decision_Procs/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     6.2 +++ b/src/HOL/Decision_Procs/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     6.3 @@ -1,2 +1,1 @@
     6.4 -
     6.5 -use_thy "Decision_Procs";
     6.6 +use_thys ["Decision_Procs"];
     7.1 --- a/src/HOL/Hahn_Banach/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     7.2 +++ b/src/HOL/Hahn_Banach/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     7.3 @@ -4,4 +4,4 @@
     7.4  The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
     7.5  *)
     7.6  
     7.7 -use_thy "Hahn_Banach";
     7.8 +use_thys ["Hahn_Banach"];
     8.1 --- a/src/HOL/Hoare_Parallel/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     8.2 +++ b/src/HOL/Hoare_Parallel/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     8.3 @@ -1,2 +1,1 @@
     8.4 -
     8.5 -use_thy "Hoare_Parallel";
     8.6 +use_thys ["Hoare_Parallel"];
     9.1 --- a/src/HOL/IMPP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     9.2 +++ b/src/HOL/IMPP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     9.3 @@ -1,7 +1,6 @@
     9.4  (*  Title:      HOL/IMPP/ROOT.ML
     9.5 -    ID:         $Id$
     9.6      Author:     David von Oheimb
     9.7      Copyright   1999 TUM
     9.8  *)
     9.9  
    9.10 -time_use_thy "EvenOdd";
    9.11 +use_thys ["EvenOdd"];
    10.1 --- a/src/HOL/IOA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    10.2 +++ b/src/HOL/IOA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/IOA/ROOT.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Tobias Nipkow & Konrad Slind
    10.7      Copyright   1994  TU Muenchen
    10.8  
    10.9 @@ -25,4 +24,4 @@
   10.10  ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   10.11  *)
   10.12  
   10.13 -use_thy "Solve";
   10.14 +use_thys ["Solve"];
    11.1 --- a/src/HOL/Imperative_HOL/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    11.2 +++ b/src/HOL/Imperative_HOL/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    11.3 @@ -1,2 +1,1 @@
    11.4 -
    11.5 -use_thy "Imperative_HOL_ex";
    11.6 +use_thys ["Imperative_HOL_ex"];
    12.1 --- a/src/HOL/Induct/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    12.2 +++ b/src/HOL/Induct/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    12.3 @@ -1,8 +1,5 @@
    12.4 -
    12.5 -(* $Id$ *)
    12.6 -
    12.7  setmp_noncritical quick_and_dirty true
    12.8 -  use_thy "Common_Patterns";
    12.9 +  use_thys ["Common_Patterns"];
   12.10  
   12.11  use_thys ["QuoDataType", "QuoNestedDataType", "Term",
   12.12    "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
    13.1 --- a/src/HOL/Lambda/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    13.2 +++ b/src/HOL/Lambda/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    13.3 @@ -11,4 +11,4 @@
    13.4  use_thys ["Eta", "StrongNorm", "Standardization"];
    13.5  if HOL_proofs < 2 then
    13.6    warning "HOL proof terms required for running theory WeakNorm"
    13.7 -else use_thy "WeakNorm";
    13.8 +else use_thys ["WeakNorm"];
    14.1 --- a/src/HOL/Lattice/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    14.2 +++ b/src/HOL/Lattice/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    14.3 @@ -1,8 +1,7 @@
    14.4  (*  Title:      HOL/Lattice/ROOT.ML
    14.5 -    ID:         $Id$
    14.6      Author:     Markus Wenzel, TU Muenchen
    14.7  
    14.8  Basic theory of lattices and orders.
    14.9  *)
   14.10  
   14.11 -time_use_thy "CompleteLattice";
   14.12 +use_thys ["CompleteLattice"];
    15.1 --- a/src/HOL/MicroJava/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    15.2 +++ b/src/HOL/MicroJava/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    15.3 @@ -1,5 +1,3 @@
    15.4 -(* $Id$ *)
    15.5 +no_document use_thys ["While_Combinator"];
    15.6  
    15.7 -no_document use_thy "While_Combinator";
    15.8 -
    15.9 -use_thy "MicroJava";
   15.10 +use_thys ["MicroJava"];
    16.1 --- a/src/HOL/Mirabelle/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    16.2 +++ b/src/HOL/Mirabelle/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    16.3 @@ -1,1 +1,1 @@
    16.4 -use_thy "Mirabelle_Test";
    16.5 +use_thys ["Mirabelle_Test"];
    17.1 --- a/src/HOL/Multivariate_Analysis/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    17.3 @@ -1,1 +1,1 @@
    17.4 -use_thy "Multivariate_Analysis";
    17.5 +use_thys ["Multivariate_Analysis"];
    18.1 --- a/src/HOL/NSA/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    18.2 +++ b/src/HOL/NSA/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    18.3 @@ -1,1 +1,1 @@
    18.4 -use_thy "NSPrimes";
    18.5 +use_thys ["NSPrimes"];
    19.1 --- a/src/HOL/NSA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    19.2 +++ b/src/HOL/NSA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    19.3 @@ -1,2 +1,1 @@
    19.4 -(* $ID$ *)
    19.5 -use_thy "Hypercomplex";
    19.6 +use_thys ["Hypercomplex"];
    20.1 --- a/src/HOL/NanoJava/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    20.2 +++ b/src/HOL/NanoJava/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    20.3 @@ -1,1 +1,1 @@
    20.4 -use_thy "Example";
    20.5 +use_thys ["Example"];
    21.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    21.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    21.3 @@ -1,4 +1,3 @@
    21.4 +use_thys ["Nominal_Examples"];
    21.5  
    21.6 -use_thy "Nominal_Examples";
    21.7 -
    21.8 -setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)
    21.9 +setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)
    22.1 --- a/src/HOL/Nominal/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    22.2 +++ b/src/HOL/Nominal/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    22.3 @@ -1,9 +1,8 @@
    22.4  (*  Title:      HOL/Nominal/ROOT.ML
    22.5 -    ID:         $Id$
    22.6      Author:     Stefan Berghofer and Christian Urban, TU Muenchen
    22.7  
    22.8  The nominal datatype package.
    22.9  *)
   22.10  
   22.11 -no_document use_thy "Infinite_Set";
   22.12 -use_thy "Nominal";
   22.13 +no_document use_thys ["Infinite_Set"];
   22.14 +use_thys ["Nominal"];
    23.1 --- a/src/HOL/Number_Theory/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    23.2 +++ b/src/HOL/Number_Theory/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    23.3 @@ -1,2 +1,1 @@
    23.4 -
    23.5 -use_thy "Number_Theory";
    23.6 +use_thys ["Number_Theory"];
    24.1 --- a/src/HOL/Probability/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    24.2 +++ b/src/HOL/Probability/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    24.3 @@ -1,1 +1,1 @@
    24.4 -use_thy "Probability";
    24.5 +use_thys ["Probability"];
    25.1 --- a/src/HOL/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    25.2 +++ b/src/HOL/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    25.3 @@ -1,5 +1,5 @@
    25.4  (* Classical Higher-order Logic -- batteries included *)
    25.5  
    25.6 -use_thy "Complex_Main";
    25.7 +use_thys ["Complex_Main"];
    25.8  
    25.9  val HOL_proofs = ! Proofterm.proofs;
    26.1 --- a/src/HOL/SET_Protocol/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    26.2 +++ b/src/HOL/SET_Protocol/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    26.3 @@ -5,5 +5,5 @@
    26.4  Root file for the SET protocol proofs.
    26.5  *)
    26.6  
    26.7 -no_document use_thy "Nat_Int_Bij";
    26.8 +no_document use_thys ["Nat_Int_Bij"];
    26.9  use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
    27.1 --- a/src/HOL/SMT/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    27.2 +++ b/src/HOL/SMT/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    27.3 @@ -1,1 +1,1 @@
    27.4 -use_thy "SMT_Examples";
    27.5 +use_thys ["SMT_Examples"];
    28.1 --- a/src/HOL/SMT/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    28.2 +++ b/src/HOL/SMT/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    28.3 @@ -1,1 +1,1 @@
    28.4 -use_thy "SMT";
    28.5 +use_thys ["SMT"];
    29.1 --- a/src/HOL/Statespace/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    29.2 +++ b/src/HOL/Statespace/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    29.3 @@ -1,1 +1,1 @@
    29.4 -use_thy "StateSpaceEx";
    29.5 \ No newline at end of file
    29.6 +use_thys ["StateSpaceEx"];
    29.7 \ No newline at end of file
    30.1 --- a/src/HOL/Subst/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    30.2 +++ b/src/HOL/Subst/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    30.3 @@ -1,7 +1,6 @@
    30.4  (*  Title:      HOL/Subst/ROOT.ML
    30.5 -    ID:         $Id$
    30.6 -    Authors:     Martin Coen, Cambridge University Computer Laboratory
    30.7 -                 Konrad Slind, TU Munich
    30.8 +    Authors:    Martin Coen, Cambridge University Computer Laboratory
    30.9 +                Konrad Slind, TU Munich
   30.10      Copyright   1993  University of Cambridge,
   30.11                  1996  TU Munich
   30.12  
   30.13 @@ -24,4 +23,4 @@
   30.14  
   30.15  *)
   30.16  
   30.17 -time_use_thy "Unify";
   30.18 +use_thys ["Unify"];
    31.1 --- a/src/HOL/TLA/Buffer/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    31.2 +++ b/src/HOL/TLA/Buffer/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    31.3 @@ -1,4 +1,1 @@
    31.4 -
    31.5 -(* $Id$ *)
    31.6 -
    31.7 -time_use_thy "DBuffer";
    31.8 +use_thys ["DBuffer"];
    32.1 --- a/src/HOL/TLA/Inc/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    32.2 +++ b/src/HOL/TLA/Inc/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    32.3 @@ -1,4 +1,1 @@
    32.4 -
    32.5 -(* $Id$ *)
    32.6 -
    32.7 -time_use_thy "Inc";
    32.8 +use_thys ["Inc"];
    33.1 --- a/src/HOL/TLA/Memory/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    33.2 +++ b/src/HOL/TLA/Memory/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    33.3 @@ -1,4 +1,1 @@
    33.4 -
    33.5 -(* $Id$ *)
    33.6 -
    33.7 -time_use_thy "MemoryImplementation";
    33.8 +use_thys ["MemoryImplementation"];
    34.1 --- a/src/HOL/TLA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    34.2 +++ b/src/HOL/TLA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    34.3 @@ -1,8 +1,7 @@
    34.4  (*  Title:      HOL/TLA/ROOT.ML
    34.5 -    ID:         $Id$
    34.6  
    34.7  Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
    34.8  *)
    34.9  
   34.10 -use_thy "TLA";
   34.11 +use_thys ["TLA"];
   34.12  
    35.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    35.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    35.3 @@ -1,13 +1,12 @@
    35.4  (*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    35.5      Copyright   1998  University of Cambridge
    35.6 -
    35.7  *)
    35.8  
    35.9  (*Verifying security protocols using UNITY*)
   35.10 -no_document use_thy "../Auth/Public";
   35.11 +no_document use_thys ["../Auth/Public"];
   35.12  
   35.13 -(*Basic meta-theory*)
   35.14 -use_thy "UNITY_Main";
   35.15 +use_thys [
   35.16 +  "UNITY_Main",     (*Basic meta-theory*)
   35.17 +  "UNITY_Examples"  (*Examples*)
   35.18 +];
   35.19  
   35.20 -(*Examples*)
   35.21 -use_thy "UNITY_Examples";
    36.1 --- a/src/HOL/Unix/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    36.2 +++ b/src/HOL/Unix/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    36.3 @@ -1,4 +1,2 @@
    36.4 -(* $Id$ *)
    36.5 -
    36.6  setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
    36.7 -  use_thy "Unix";
    36.8 +  use_thys ["Unix"];
    37.1 --- a/src/HOL/W0/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    37.2 +++ b/src/HOL/W0/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    37.3 @@ -1,2 +1,1 @@
    37.4 -
    37.5 -use_thy "W0";
    37.6 +use_thys ["W0"];
    38.1 --- a/src/HOL/Word/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    38.2 +++ b/src/HOL/Word/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    38.3 @@ -1,1 +1,1 @@
    38.4 -use_thy "WordExamples";
    38.5 +use_thys ["WordExamples"];
    39.1 --- a/src/HOL/Word/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    39.2 +++ b/src/HOL/Word/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    39.3 @@ -1,1 +1,1 @@
    39.4 -use_thy "Word";
    39.5 +use_thys ["Word"];
    40.1 --- a/src/HOL/ZF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    40.2 +++ b/src/HOL/ZF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    40.3 @@ -1,6 +1,1 @@
    40.4 -(*  Title:      HOL/ZF/ROOT.ML
    40.5 -    ID:         $Id$
    40.6 -*)
    40.7 -
    40.8 -use_thy "MainZF";
    40.9 -use_thy "Games";
   40.10 +use_thys ["MainZF", "Games"];
    41.1 --- a/src/HOL/base.ML	Wed Nov 11 09:02:37 2009 +0100
    41.2 +++ b/src/HOL/base.ML	Wed Nov 11 14:15:11 2009 +0100
    41.3 @@ -1,2 +1,2 @@
    41.4  (*side-entry for HOL-Base*)
    41.5 -use_thy "HOL";
    41.6 +use_thys ["HOL"];
    42.1 --- a/src/HOL/main.ML	Wed Nov 11 09:02:37 2009 +0100
    42.2 +++ b/src/HOL/main.ML	Wed Nov 11 14:15:11 2009 +0100
    42.3 @@ -1,2 +1,2 @@
    42.4  (*side-entry for HOL-Main*)
    42.5 -use_thy "Main";
    42.6 +use_thys ["Main"];
    43.1 --- a/src/HOL/plain.ML	Wed Nov 11 09:02:37 2009 +0100
    43.2 +++ b/src/HOL/plain.ML	Wed Nov 11 14:15:11 2009 +0100
    43.3 @@ -1,2 +1,2 @@
    43.4  (*side-entry for HOL-Plain*)
    43.5 -use_thy "Plain";
    43.6 +use_thys ["Plain"];
    44.1 --- a/src/HOLCF/IOA/ABP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    44.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    44.3 @@ -1,11 +1,11 @@
    44.4  (*  Title:      HOLCF/IOA/ABP/ROOT.ML
    44.5 -    ID:         $Id$
    44.6      Author:     Olaf Mueller
    44.7  
    44.8  This is the ROOT file for the Alternating Bit Protocol performed in
    44.9 -I/O-Automata.  *)
   44.10 +I/O-Automata.
   44.11 +*)
   44.12  
   44.13  goals_limit := 1;
   44.14  
   44.15  use "Check.ML";
   44.16 -time_use_thy "Correctness";
   44.17 +use_thys ["Correctness"];
    45.1 --- a/src/HOLCF/IOA/NTP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    45.2 +++ b/src/HOLCF/IOA/NTP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      HOLCF/IOA/NTP/ROOT.ML
    45.5 -    ID:         $Id$
    45.6      Author:     Tobias Nipkow & Konrad Slind
    45.7  
    45.8  This is the ROOT file for a network transmission protocol (NTP
    45.9 @@ -7,4 +6,4 @@
   45.10  Mueller.
   45.11  *)
   45.12  
   45.13 -use_thy "Correctness";
   45.14 +use_thys ["Correctness"];
    46.1 --- a/src/HOLCF/IOA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    46.2 +++ b/src/HOLCF/IOA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    46.3 @@ -1,9 +1,8 @@
    46.4  (*  Title:      HOLCF/IOA/ROOT.ML
    46.5 -    ID:         $Id$
    46.6      Author:     Olaf Mueller
    46.7  
    46.8  Formalization of a semantic model of I/O-Automata.  See README.html
    46.9  for details.
   46.10  *)
   46.11  
   46.12 -time_use_thy "meta_theory/Abstraction";
   46.13 +use_thys ["meta_theory/Abstraction"];
    47.1 --- a/src/HOLCF/IOA/Storage/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    47.2 +++ b/src/HOLCF/IOA/Storage/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    47.3 @@ -1,5 +1,4 @@
    47.4  (*  Title:      HOLCF/IOA/Storage/ROOT.ML
    47.5 -    ID:         $Id$
    47.6      Author:     Olaf Mueller
    47.7  
    47.8  Memory storage case study.
    47.9 @@ -7,4 +6,4 @@
   47.10  
   47.11  goals_limit := 1;
   47.12  
   47.13 -time_use_thy "Correctness";
   47.14 +use_thys ["Correctness"];
    48.1 --- a/src/HOLCF/IOA/ex/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    48.2 +++ b/src/HOLCF/IOA/ex/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    48.3 @@ -1,7 +1,5 @@
    48.4  (*  Title:      HOLCF/IOA/ex/ROOT.ML
    48.5 -    ID:         $Id$
    48.6      Author:     Olaf Mueller
    48.7  *)
    48.8  
    48.9 -time_use_thy "TrivEx";
   48.10 -time_use_thy "TrivEx2";
   48.11 +use_thys ["TrivEx", "TrivEx2"];
    49.1 --- a/src/HOLCF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    49.2 +++ b/src/HOLCF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    49.3 @@ -1,10 +1,9 @@
    49.4  (*  Title:      HOLCF/ROOT.ML
    49.5 -    ID:         $Id$
    49.6      Author:     Franz Regensburger
    49.7  
    49.8  HOLCF -- a semantic extension of HOL by the LCF logic.
    49.9  *)
   49.10  
   49.11 -no_document use_thy "Nat_Int_Bij";
   49.12 +no_document use_thys ["Nat_Int_Bij"];
   49.13  
   49.14 -use_thy "HOLCF";
   49.15 +use_thys ["HOLCF"];
    50.1 --- a/src/LCF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    50.2 +++ b/src/LCF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    50.3 @@ -1,8 +1,7 @@
    50.4  (*  Title:      LCF/ROOT.ML
    50.5 -    ID:         $Id$
    50.6      Author:     Tobias Nipkow
    50.7      Copyright   1992  University of Cambridge
    50.8  *)
    50.9  
   50.10 -use_thy "LCF";
   50.11 +use_thys ["LCF"];
   50.12  
    51.1 --- a/src/ZF/Coind/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    51.2 +++ b/src/ZF/Coind/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    51.3 @@ -1,5 +1,4 @@
    51.4  (*  Title:      ZF/Coind/ROOT.ML
    51.5 -    ID:         $Id$
    51.6      Author:     Jacob Frost, Cambridge University Computer Laboratory
    51.7      Copyright   1995  University of Cambridge
    51.8  
    51.9 @@ -13,4 +12,4 @@
   51.10      Report, Computer Lab, University of Cambridge (1995).
   51.11  *)
   51.12  
   51.13 -time_use_thy "ECR";
   51.14 +use_thys ["ECR"];
    52.1 --- a/src/ZF/IMP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    52.2 +++ b/src/ZF/IMP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    52.3 @@ -1,5 +1,4 @@
    52.4  (*  Title:      ZF/IMP/ROOT.ML
    52.5 -    ID:         $Id$
    52.6      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    52.7      Copyright   1994 TUM
    52.8  
    52.9 @@ -12,4 +11,4 @@
   52.10  
   52.11  *)
   52.12  
   52.13 -time_use_thy "Equiv";
   52.14 +use_thys ["Equiv"];
    53.1 --- a/src/ZF/Resid/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
    53.2 +++ b/src/ZF/Resid/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
    53.3 @@ -1,5 +1,4 @@
    53.4 -(*  Title:      ZF/Resid/ROOT
    53.5 -    ID:         $Id$
    53.6 +(*  Title:      ZF/Resid/ROOT.ML
    53.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    53.8      Copyright   1995  University of Cambridge
    53.9  
   53.10 @@ -12,4 +11,4 @@
   53.11  J. Functional Programming 4(3) 1994, 371-394.
   53.12  *)
   53.13  
   53.14 -time_use_thy "Confluence";
   53.15 +use_thys ["Confluence"];