1.1 --- a/src/HOL/IsaMakefile	Wed Jun 13 16:30:12 2001 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sat Jun 16 20:06:42 2001 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    HOL-MicroJava \
     1.5    HOL-MiniML \
     1.6    HOL-Modelcheck \
     1.7 +  HOL-NanoJava \
     1.8    HOL-NumberTheory \
     1.9    HOL-Prolog \
    1.10    HOL-Subst \
    1.11 @@ -460,6 +461,15 @@
    1.12    MicroJava/document/root.bib MicroJava/document/root.tex
    1.13  	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
    1.14  
    1.15 +## HOL-NanoJava
    1.16 +
    1.17 +HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
    1.18 +
    1.19 +$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
    1.20 +  NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
    1.21 +  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
    1.22 +  NanoJava/document/root.bib NanoJava/document/root.tex
    1.23 +	@$(ISATOOL) usedir $(OUT)/HOL NanoJava
    1.24  
    1.25  ## HOL-CTL
    1.26  
    1.27 @@ -581,7 +591,7 @@
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 -	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
    1.32 +	@rm -f  $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
    1.33  		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
    1.34  		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
    1.35  		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
    1.36 @@ -589,8 +599,8 @@
    1.37  		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.38  		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.39  		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.40 -		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
    1.41 -		$(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
    1.42 +		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-CTL.gz \
    1.43 +		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
    1.44  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
    1.45  		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
    1.46  		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \