# HG changeset patch
# User schirmer
# Date 1012236733 -3600
# Node ID 21225338f8db2690c189c242e45a5d3c1567804f
# Parent  00d4a435777f03d09c2ef071a766fe3cd94f55c7
Bali added

diff -r 00d4a435777f -r 21225338f8db src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jan 28 17:00:19 2002 +0100
+++ b/src/HOL/IsaMakefile	Mon Jan 28 17:52:13 2002 +0100
@@ -15,6 +15,7 @@
   HOL-Algebra \
   HOL-Auth \
   HOL-AxClasses \
+  HOL-Bali \
   HOL-CTL \
   HOL-GroupTheory \
       HOL-Real-HahnBanach \
@@ -489,6 +490,20 @@
 	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
 
 
+## HOL-Bali
+
+HOL-Bali: HOL $(LOG)/HOL-Bali.gz
+
+$(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/WellType.thy Bali/document/root.tex
+	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
+
+
 ## HOL-CTL
 
 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
@@ -618,7 +633,8 @@
 		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
 		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
-		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-CTL.gz \
+		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
+                $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \
 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \