--- a/src/HOL/Bali/ROOT.ML Mon Jul 30 19:22:27 2007 +0200
+++ b/src/HOL/Bali/ROOT.ML Mon Jul 30 19:46:13 2007 +0200
@@ -1,12 +1,9 @@
-(* Title: isabelle/Bali/ROOT3.ML
+(* Title: HOL/Bali/ROOT.ML
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
-The Hoare logic for Bali
+The Hoare logic for Bali.
*)
-use_thy "AxExample";
-use_thy "AxSound";
-use_thy "AxCompl";
-use_thy "Trans";
+use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
--- a/src/HOL/MicroJava/ROOT.ML Mon Jul 30 19:22:27 2007 +0200
+++ b/src/HOL/MicroJava/ROOT.ML Mon Jul 30 19:46:13 2007 +0200
@@ -1,20 +1,8 @@
-goals_limit := 1;
-
-add_path "J";
-add_path "JVM";
-add_path "BV";
-add_path "Comp";
+(* $Id$ *)
no_document use_thy "While_Combinator";
-use_thy "JTypeSafe";
-use_thy "Example";
-use_thy "JListExample";
-use_thy "JVMListExample";
-use_thy "JVMDefensive";
-use_thy "LBVJVM";
-use_thy "BVNoTypeError";
-use_thy "BVExample";
-
-use_thy "CorrComp";
-use_thy "CorrCompTp";
+use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",
+ "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",
+ "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",
+ "Comp/CorrCompTp"];