# HG changeset patch
# User haftmann
# Date 1253541653 -7200
# Node ID 9b19cbb0af28d35c735be7de7c5a949d256f6561
# Parent  4ba4bfa087490964c51ce1ca956fd1465f2ebfc3
added session theory for Bali

diff -r 4ba4bfa08749 -r 9b19cbb0af28 src/HOL/Bali/Bali.thy
--- /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
diff -r 4ba4bfa08749 -r 9b19cbb0af28 src/HOL/Bali/ROOT.ML
--- 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"