# HG changeset patch
# User wenzelm
# Date 1300054358 -3600
# Node ID 8a399da4cde1edf8bb49727fbf9da143a0b40947
# Parent  b460124855b85b45ad4222e198695c2a88d93221
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;

diff -r b460124855b8 -r 8a399da4cde1 src/HOL/Bali/Bali.thy
--- a/src/HOL/Bali/Bali.thy	Sun Mar 13 22:55:50 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  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 b460124855b8 -r 8a399da4cde1 src/HOL/Bali/ROOT.ML
--- a/src/HOL/Bali/ROOT.ML	Sun Mar 13 22:55:50 2011 +0100
+++ b/src/HOL/Bali/ROOT.ML	Sun Mar 13 23:12:38 2011 +0100
@@ -1,1 +1,1 @@
-use_thys ["Bali"];
+use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
diff -r b460124855b8 -r 8a399da4cde1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Mar 13 22:55:50 2011 +0100
+++ b/src/HOL/IsaMakefile	Sun Mar 13 23:12:38 2011 +0100
@@ -992,15 +992,14 @@
 
 HOL-Bali: HOL $(LOG)/HOL-Bali.gz
 
-$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy		\
-  Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy	\
-  Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy	\
-  Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML		\
-  Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy		\
-  Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy	\
-  Bali/WellForm.thy Bali/DefiniteAssignment.thy				\
-  Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy			\
-  Bali/document/root.tex
+$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
+  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
+  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
+  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
+  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
+  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
+  Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
+  Bali/WellType.thy Bali/document/root.tex
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali