--- a/src/CTT/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/CTT/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/FOL/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/FOL/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,3 +1,3 @@
(* First-Order Logic with Natural Deduction *)
-use_thy "FOL";
+use_thys ["FOL"];
--- a/src/FOLP/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/FOLP/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/Bali/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Bali/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Bali"
+use_thys ["Bali"];
--- a/src/HOL/Boogie/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Boogie/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Boogie";
+use_thys ["Boogie"];
--- a/src/HOL/Decision_Procs/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Decision_Procs/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Decision_Procs";
+use_thys ["Decision_Procs"];
--- a/src/HOL/Hahn_Banach/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Hahn_Banach/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -4,4 +4,4 @@
The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)
-use_thy "Hahn_Banach";
+use_thys ["Hahn_Banach"];
--- a/src/HOL/Hoare_Parallel/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Hoare_Parallel/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Hoare_Parallel";
+use_thys ["Hoare_Parallel"];
--- a/src/HOL/IMPP/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/IMPP/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/IOA/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/IOA/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/Imperative_HOL/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Imperative_HOL/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Imperative_HOL_ex";
+use_thys ["Imperative_HOL_ex"];
--- a/src/HOL/Induct/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Induct/ROOT.ML Wed Nov 11 17:27:48 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",
--- a/src/HOL/Lambda/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Lambda/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/Lattice/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Lattice/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/MicroJava/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/Mirabelle/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Mirabelle/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Mirabelle_Test";
+use_thys ["Mirabelle_Test"];
--- a/src/HOL/Multivariate_Analysis/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Multivariate_Analysis";
+use_thys ["Multivariate_Analysis"];
--- a/src/HOL/NSA/Examples/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/NSA/Examples/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "NSPrimes";
+use_thys ["NSPrimes"];
--- a/src/HOL/NSA/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/NSA/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-(* $ID$ *)
-use_thy "Hypercomplex";
+use_thys ["Hypercomplex"];
--- a/src/HOL/NanoJava/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/NanoJava/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Example";
+use_thys ["Example"];
--- a/src/HOL/Nominal/Examples/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML Wed Nov 11 17:27:48 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*)
--- a/src/HOL/Nominal/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Nominal/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/Number_Theory/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Number_Theory/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "Number_Theory";
+use_thys ["Number_Theory"];
--- a/src/HOL/Probability/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Probability/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Probability";
+use_thys ["Probability"];
--- a/src/HOL/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/ROOT.ML Wed Nov 11 17:27:48 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;
--- a/src/HOL/SET_Protocol/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/SET_Protocol/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/SMT/Examples/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/SMT/Examples/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "SMT_Examples";
+use_thys ["SMT_Examples"];
--- a/src/HOL/SMT/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/SMT/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "SMT";
+use_thys ["SMT"];
--- a/src/HOL/Statespace/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Statespace/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "StateSpaceEx";
\ No newline at end of file
+use_thys ["StateSpaceEx"];
\ No newline at end of file
--- a/src/HOL/Subst/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Subst/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/TLA/Buffer/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/TLA/Buffer/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
-time_use_thy "DBuffer";
+use_thys ["DBuffer"];
--- a/src/HOL/TLA/Inc/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/TLA/Inc/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
-time_use_thy "Inc";
+use_thys ["Inc"];
--- a/src/HOL/TLA/Memory/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/TLA/Memory/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,4 +1,1 @@
-
-(* $Id$ *)
-
-time_use_thy "MemoryImplementation";
+use_thys ["MemoryImplementation"];
--- a/src/HOL/TLA/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/TLA/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOL/UNITY/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/UNITY/ROOT.ML Wed Nov 11 17:27:48 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";
--- a/src/HOL/Unix/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Unix/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,4 +1,2 @@
-(* $Id$ *)
-
setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
- use_thy "Unix";
+ use_thys ["Unix"];
--- a/src/HOL/W0/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/W0/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,1 @@
-
-use_thy "W0";
+use_thys ["W0"];
--- a/src/HOL/Word/Examples/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Word/Examples/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "WordExamples";
+use_thys ["WordExamples"];
--- a/src/HOL/Word/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/Word/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "Word";
+use_thys ["Word"];
--- a/src/HOL/ZF/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/ZF/ROOT.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,6 +1,1 @@
-(* Title: HOL/ZF/ROOT.ML
- ID: $Id$
-*)
-
-use_thy "MainZF";
-use_thy "Games";
+use_thys ["MainZF", "Games"];
--- a/src/HOL/base.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/base.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,2 @@
(*side-entry for HOL-Base*)
-use_thy "HOL";
+use_thys ["HOL"];
--- a/src/HOL/main.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/main.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,2 @@
(*side-entry for HOL-Main*)
-use_thy "Main";
+use_thys ["Main"];
--- a/src/HOL/plain.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOL/plain.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1,2 +1,2 @@
(*side-entry for HOL-Plain*)
-use_thy "Plain";
+use_thys ["Plain"];
--- a/src/HOLCF/IOA/ABP/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOLCF/IOA/ABP/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOLCF/IOA/NTP/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOLCF/IOA/NTP/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOLCF/IOA/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOLCF/IOA/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOLCF/IOA/Storage/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOLCF/IOA/Storage/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOLCF/IOA/ex/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOLCF/IOA/ex/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/HOLCF/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/HOLCF/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/LCF/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/LCF/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/ZF/Coind/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/ZF/Coind/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/ZF/IMP/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/ZF/IMP/ROOT.ML Wed Nov 11 17:27:48 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"];
--- a/src/ZF/Resid/ROOT.ML Wed Nov 11 16:19:28 2009 +0100
+++ b/src/ZF/Resid/ROOT.ML Wed Nov 11 17:27:48 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"];