1.1 --- a/src/HOL/IsaMakefile	Mon Jan 28 17:00:19 2002 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jan 28 17:52:13 2002 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    HOL-Algebra \
     1.5    HOL-Auth \
     1.6    HOL-AxClasses \
     1.7 +  HOL-Bali \
     1.8    HOL-CTL \
     1.9    HOL-GroupTheory \
    1.10        HOL-Real-HahnBanach \
    1.11 @@ -489,6 +490,20 @@
    1.12  	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
    1.13  
    1.14  
    1.15 +## HOL-Bali
    1.16 +
    1.17 +HOL-Bali: HOL $(LOG)/HOL-Bali.gz
    1.18 +
    1.19 +$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
    1.20 +  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
    1.21 +  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
    1.22 +  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
    1.23 +  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
    1.24 +  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
    1.25 +  Bali/WellType.thy Bali/document/root.tex
    1.26 +	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
    1.27 +
    1.28 +
    1.29  ## HOL-CTL
    1.30  
    1.31  HOL-CTL: HOL $(LOG)/HOL-CTL.gz
    1.32 @@ -618,7 +633,8 @@
    1.33  		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.34  		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.35  		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.36 -		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-CTL.gz \
    1.37 +		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
    1.38 +                $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \
    1.39  		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
    1.40  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
    1.41  		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \