# HG changeset patch
# User wenzelm
# Date 1257945311 -3600
# Node ID 261abc2e3155f2c4dc4dee59324027940854956c
# Parent  5c0024338ceff4063eafd58621ec48dc9b14cc2e
uniform use of simultabeous use_thys;

diff -r 5c0024338cef -r 261abc2e3155 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/CTT/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      CTT/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
 
-use_thy "Main";
+use_thys ["Main"];
 
diff -r 5c0024338cef -r 261abc2e3155 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/FOL/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,3 +1,3 @@
 (* First-Order Logic with Natural Deduction *)
 
-use_thy "FOL";
+use_thys ["FOL"];
diff -r 5c0024338cef -r 261abc2e3155 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/FOLP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,6 +1,5 @@
 (*  Title:      FOLP/ROOT.ML
-    ID:         $Id$
-    Author:     martin Coen, Cambridge University Computer Laboratory
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Modifed version of Lawrence Paulson's FOL that contains proof terms.
@@ -8,5 +7,5 @@
 Presence of unknown proof term means that matching does not behave as expected.
 *)
 
-use_thy "FOLP";
+use_thys ["FOLP"];
 
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Bali/ROOT.ML
--- a/src/HOL/Bali/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Bali/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Bali"
+use_thys ["Bali"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Boogie/ROOT.ML
--- a/src/HOL/Boogie/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Boogie/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Boogie";
+use_thys ["Boogie"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Decision_Procs/ROOT.ML
--- a/src/HOL/Decision_Procs/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Decision_Procs/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Decision_Procs";
+use_thys ["Decision_Procs"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Hahn_Banach/ROOT.ML
--- a/src/HOL/Hahn_Banach/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Hahn_Banach/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -4,4 +4,4 @@
 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
-use_thy "Hahn_Banach";
+use_thys ["Hahn_Banach"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Hoare_Parallel/ROOT.ML
--- a/src/HOL/Hoare_Parallel/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Hoare_Parallel/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Hoare_Parallel";
+use_thys ["Hoare_Parallel"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/IMPP/ROOT.ML
--- a/src/HOL/IMPP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/IMPP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,7 +1,6 @@
 (*  Title:      HOL/IMPP/ROOT.ML
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 TUM
 *)
 
-time_use_thy "EvenOdd";
+use_thys ["EvenOdd"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/IOA/ROOT.ML
--- a/src/HOL/IOA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/IOA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/IOA/ROOT.ML
-    ID:         $Id$
     Author:     Tobias Nipkow & Konrad Slind
     Copyright   1994  TU Muenchen
 
@@ -25,4 +24,4 @@
 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
 *)
 
-use_thy "Solve";
+use_thys ["Solve"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Imperative_HOL/ROOT.ML
--- a/src/HOL/Imperative_HOL/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Imperative_HOL/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Imperative_HOL_ex";
+use_thys ["Imperative_HOL_ex"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Induct/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,8 +1,5 @@
-
-(* $Id$ *)
-
 setmp_noncritical quick_and_dirty true
-  use_thy "Common_Patterns";
+  use_thys ["Common_Patterns"];
 
 use_thys ["QuoDataType", "QuoNestedDataType", "Term",
   "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -11,4 +11,4 @@
 use_thys ["Eta", "StrongNorm", "Standardization"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"
-else use_thy "WeakNorm";
+else use_thys ["WeakNorm"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Lattice/ROOT.ML
--- a/src/HOL/Lattice/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Lattice/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOL/Lattice/ROOT.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Basic theory of lattices and orders.
 *)
 
-time_use_thy "CompleteLattice";
+use_thys ["CompleteLattice"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
+no_document use_thys ["While_Combinator"];
 
-no_document use_thy "While_Combinator";
-
-use_thy "MicroJava";
+use_thys ["MicroJava"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Mirabelle/ROOT.ML
--- a/src/HOL/Mirabelle/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Mirabelle/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Mirabelle_Test";
+use_thys ["Mirabelle_Test"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Multivariate_Analysis/ROOT.ML
--- a/src/HOL/Multivariate_Analysis/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Multivariate_Analysis";
+use_thys ["Multivariate_Analysis"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/NSA/Examples/ROOT.ML
--- a/src/HOL/NSA/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/NSA/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "NSPrimes";
+use_thys ["NSPrimes"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/NSA/ROOT.ML
--- a/src/HOL/NSA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/NSA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-(* $ID$ *)
-use_thy "Hypercomplex";
+use_thys ["Hypercomplex"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/NanoJava/ROOT.ML
--- a/src/HOL/NanoJava/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/NanoJava/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Example";
+use_thys ["Example"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,4 +1,3 @@
+use_thys ["Nominal_Examples"];
 
-use_thy "Nominal_Examples";
-
-setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)
+setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Nominal/ROOT.ML
--- a/src/HOL/Nominal/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Nominal/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,9 +1,8 @@
 (*  Title:      HOL/Nominal/ROOT.ML
-    ID:         $Id$
     Author:     Stefan Berghofer and Christian Urban, TU Muenchen
 
 The nominal datatype package.
 *)
 
-no_document use_thy "Infinite_Set";
-use_thy "Nominal";
+no_document use_thys ["Infinite_Set"];
+use_thys ["Nominal"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Number_Theory/ROOT.ML
--- a/src/HOL/Number_Theory/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Number_Theory/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Number_Theory";
+use_thys ["Number_Theory"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Probability/ROOT.ML
--- a/src/HOL/Probability/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Probability/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Probability";
+use_thys ["Probability"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,5 @@
 (* Classical Higher-order Logic -- batteries included *)
 
-use_thy "Complex_Main";
+use_thys ["Complex_Main"];
 
 val HOL_proofs = ! Proofterm.proofs;
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/SET_Protocol/ROOT.ML
--- a/src/HOL/SET_Protocol/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/SET_Protocol/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -5,5 +5,5 @@
 Root file for the SET protocol proofs.
 *)
 
-no_document use_thy "Nat_Int_Bij";
+no_document use_thys ["Nat_Int_Bij"];
 use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/SMT/Examples/ROOT.ML
--- a/src/HOL/SMT/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/SMT/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "SMT_Examples";
+use_thys ["SMT_Examples"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/SMT/ROOT.ML
--- a/src/HOL/SMT/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/SMT/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "SMT";
+use_thys ["SMT"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Statespace/ROOT.ML
--- a/src/HOL/Statespace/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Statespace/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "StateSpaceEx";
\ No newline at end of file
+use_thys ["StateSpaceEx"];
\ No newline at end of file
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Subst/ROOT.ML
--- a/src/HOL/Subst/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Subst/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Subst/ROOT.ML
-    ID:         $Id$
-    Authors:     Martin Coen, Cambridge University Computer Laboratory
-                 Konrad Slind, TU Munich
+    Authors:    Martin Coen, Cambridge University Computer Laboratory
+                Konrad Slind, TU Munich
     Copyright   1993  University of Cambridge,
                 1996  TU Munich
 
@@ -24,4 +23,4 @@
 
 *)
 
-time_use_thy "Unify";
+use_thys ["Unify"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/TLA/Buffer/ROOT.ML
--- a/src/HOL/TLA/Buffer/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/TLA/Buffer/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
-time_use_thy "DBuffer";
+use_thys ["DBuffer"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/TLA/Inc/ROOT.ML
--- a/src/HOL/TLA/Inc/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/TLA/Inc/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
-time_use_thy "Inc";
+use_thys ["Inc"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/TLA/Memory/ROOT.ML
--- a/src/HOL/TLA/Memory/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/TLA/Memory/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
-time_use_thy "MemoryImplementation";
+use_thys ["MemoryImplementation"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/TLA/ROOT.ML
--- a/src/HOL/TLA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/TLA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOL/TLA/ROOT.ML
-    ID:         $Id$
 
 Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
 *)
 
-use_thy "TLA";
+use_thys ["TLA"];
 
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,13 +1,12 @@
 (*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
-
 *)
 
 (*Verifying security protocols using UNITY*)
-no_document use_thy "../Auth/Public";
+no_document use_thys ["../Auth/Public"];
 
-(*Basic meta-theory*)
-use_thy "UNITY_Main";
+use_thys [
+  "UNITY_Main",     (*Basic meta-theory*)
+  "UNITY_Examples"  (*Examples*)
+];
 
-(*Examples*)
-use_thy "UNITY_Examples";
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Unix/ROOT.ML
--- a/src/HOL/Unix/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Unix/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,4 +1,2 @@
-(* $Id$ *)
-
 setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
-  use_thy "Unix";
+  use_thys ["Unix"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/W0/ROOT.ML
--- a/src/HOL/W0/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/W0/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "W0";
+use_thys ["W0"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Word/Examples/ROOT.ML
--- a/src/HOL/Word/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Word/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "WordExamples";
+use_thys ["WordExamples"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/Word/ROOT.ML
--- a/src/HOL/Word/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Word/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Word";
+use_thys ["Word"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/ZF/ROOT.ML
--- a/src/HOL/ZF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/ZF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,6 +1,1 @@
-(*  Title:      HOL/ZF/ROOT.ML
-    ID:         $Id$
-*)
-
-use_thy "MainZF";
-use_thy "Games";
+use_thys ["MainZF", "Games"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/base.ML
--- a/src/HOL/base.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/base.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,2 @@
 (*side-entry for HOL-Base*)
-use_thy "HOL";
+use_thys ["HOL"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/main.ML
--- a/src/HOL/main.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/main.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,2 @@
 (*side-entry for HOL-Main*)
-use_thy "Main";
+use_thys ["Main"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOL/plain.ML
--- a/src/HOL/plain.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/plain.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,2 +1,2 @@
 (*side-entry for HOL-Plain*)
-use_thy "Plain";
+use_thys ["Plain"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOLCF/IOA/ABP/ROOT.ML
--- a/src/HOLCF/IOA/ABP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOLCF/IOA/ABP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,11 +1,11 @@
 (*  Title:      HOLCF/IOA/ABP/ROOT.ML
-    ID:         $Id$
     Author:     Olaf Mueller
 
 This is the ROOT file for the Alternating Bit Protocol performed in
-I/O-Automata.  *)
+I/O-Automata.
+*)
 
 goals_limit := 1;
 
 use "Check.ML";
-time_use_thy "Correctness";
+use_thys ["Correctness"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOLCF/IOA/NTP/ROOT.ML
--- a/src/HOLCF/IOA/NTP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOLCF/IOA/NTP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/IOA/NTP/ROOT.ML
-    ID:         $Id$
     Author:     Tobias Nipkow & Konrad Slind
 
 This is the ROOT file for a network transmission protocol (NTP
@@ -7,4 +6,4 @@
 Mueller.
 *)
 
-use_thy "Correctness";
+use_thys ["Correctness"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOLCF/IOA/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/IOA/ROOT.ML
-    ID:         $Id$
     Author:     Olaf Mueller
 
 Formalization of a semantic model of I/O-Automata.  See README.html
 for details.
 *)
 
-time_use_thy "meta_theory/Abstraction";
+use_thys ["meta_theory/Abstraction"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOLCF/IOA/Storage/ROOT.ML
--- a/src/HOLCF/IOA/Storage/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOLCF/IOA/Storage/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/IOA/Storage/ROOT.ML
-    ID:         $Id$
     Author:     Olaf Mueller
 
 Memory storage case study.
@@ -7,4 +6,4 @@
 
 goals_limit := 1;
 
-time_use_thy "Correctness";
+use_thys ["Correctness"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOLCF/IOA/ex/ROOT.ML
--- a/src/HOLCF/IOA/ex/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOLCF/IOA/ex/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOLCF/IOA/ex/ROOT.ML
-    ID:         $Id$
     Author:     Olaf Mueller
 *)
 
-time_use_thy "TrivEx";
-time_use_thy "TrivEx2";
+use_thys ["TrivEx", "TrivEx2"];
diff -r 5c0024338cef -r 261abc2e3155 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOLCF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/ROOT.ML
-    ID:         $Id$
     Author:     Franz Regensburger
 
 HOLCF -- a semantic extension of HOL by the LCF logic.
 *)
 
-no_document use_thy "Nat_Int_Bij";
+no_document use_thys ["Nat_Int_Bij"];
 
-use_thy "HOLCF";
+use_thys ["HOLCF"];
diff -r 5c0024338cef -r 261abc2e3155 src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/LCF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      LCF/ROOT.ML
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 *)
 
-use_thy "LCF";
+use_thys ["LCF"];
 
diff -r 5c0024338cef -r 261abc2e3155 src/ZF/Coind/ROOT.ML
--- a/src/ZF/Coind/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/ZF/Coind/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Coind/ROOT.ML
-    ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -13,4 +12,4 @@
     Report, Computer Lab, University of Cambridge (1995).
 *)
 
-time_use_thy "ECR";
+use_thys ["ECR"];
diff -r 5c0024338cef -r 261abc2e3155 src/ZF/IMP/ROOT.ML
--- a/src/ZF/IMP/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/ZF/IMP/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/IMP/ROOT.ML
-    ID:         $Id$
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
@@ -12,4 +11,4 @@
 
 *)
 
-time_use_thy "Equiv";
+use_thys ["Equiv"];
diff -r 5c0024338cef -r 261abc2e3155 src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/ZF/Resid/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,5 +1,4 @@
-(*  Title:      ZF/Resid/ROOT
-    ID:         $Id$
+(*  Title:      ZF/Resid/ROOT.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -12,4 +11,4 @@
 J. Functional Programming 4(3) 1994, 371-394.
 *)
 
-time_use_thy "Confluence";
+use_thys ["Confluence"];