# HG changeset patch
# User wenzelm
# Date 1185817573 -7200
# Node ID 373727835757dbdcc91839d2dd8fda4eb6400746
# Parent  8b9e5d776ef3534ce897939fd69143eb166706ba
simultaneous use_thys;
tuned;

diff -r 8b9e5d776ef3 -r 373727835757 src/HOL/Bali/ROOT.ML
--- 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"];
diff -r 8b9e5d776ef3 -r 373727835757 src/HOL/MicroJava/ROOT.ML
--- 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"];