1.1 --- a/src/HOL/Bali/ROOT.ML	Mon Jul 30 19:22:27 2007 +0200
     1.2 +++ b/src/HOL/Bali/ROOT.ML	Mon Jul 30 19:46:13 2007 +0200
     1.3 @@ -1,12 +1,9 @@
     1.4 -(*  Title:      isabelle/Bali/ROOT3.ML
     1.5 +(*  Title:      HOL/Bali/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author:     David von Oheimb
     1.8      Copyright   1999 Technische Universitaet Muenchen
     1.9  
    1.10 -The Hoare logic for Bali
    1.11 +The Hoare logic for Bali.
    1.12  *)
    1.13  
    1.14 -use_thy "AxExample";
    1.15 -use_thy "AxSound";
    1.16 -use_thy "AxCompl";
    1.17 -use_thy "Trans";
    1.18 +use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];

     2.1 --- a/src/HOL/MicroJava/ROOT.ML	Mon Jul 30 19:22:27 2007 +0200
     2.2 +++ b/src/HOL/MicroJava/ROOT.ML	Mon Jul 30 19:46:13 2007 +0200
     2.3 @@ -1,20 +1,8 @@
     2.4 -goals_limit := 1;
     2.5 -
     2.6 -add_path "J";
     2.7 -add_path "JVM";
     2.8 -add_path "BV";
     2.9 -add_path "Comp";
    2.10 +(* $Id$ *)
    2.11  
    2.12  no_document use_thy "While_Combinator";
    2.13  
    2.14 -use_thy "JTypeSafe";
    2.15 -use_thy "Example";
    2.16 -use_thy "JListExample";
    2.17 -use_thy "JVMListExample";
    2.18 -use_thy "JVMDefensive";
    2.19 -use_thy "LBVJVM";
    2.20 -use_thy "BVNoTypeError";
    2.21 -use_thy "BVExample";
    2.22 -
    2.23 -use_thy "CorrComp";
    2.24 -use_thy "CorrCompTp";
    2.25 +use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",
    2.26 +  "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",
    2.27 +  "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",
    2.28 +  "Comp/CorrCompTp"];