--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Bali/Bali.thy Mon Sep 21 16:00:53 2009 +0200
@@ -0,0 +1,11 @@
+(* Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+header {* The Hoare logic for Bali. *}
+
+theory Bali
+imports AxExample AxSound AxCompl Trans
+begin
+
+end
--- a/src/HOL/Bali/ROOT.ML Mon Sep 21 16:00:34 2009 +0200
+++ b/src/HOL/Bali/ROOT.ML Mon Sep 21 16:00:53 2009 +0200
@@ -1,9 +1,2 @@
-(* Title: HOL/Bali/ROOT.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-The Hoare logic for Bali.
-*)
-
-use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
+use_thy "Bali"