src/HOL/Bali/ROOT.ML
changeset 24073 373727835757
parent 16297 928e95c867d6
child 32634 9b19cbb0af28
--- 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"];