src/HOL/IsaMakefile
changeset 11376 bf98ad1c22c6
parent 11370 680946254afe
child 11394 e88c2c89f98e
--- a/src/HOL/IsaMakefile	Wed Jun 13 16:30:12 2001 +0200
+++ b/src/HOL/IsaMakefile	Sat Jun 16 20:06:42 2001 +0200
@@ -31,6 +31,7 @@
   HOL-MicroJava \
   HOL-MiniML \
   HOL-Modelcheck \
+  HOL-NanoJava \
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-Subst \
@@ -460,6 +461,15 @@
   MicroJava/document/root.bib MicroJava/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
 
+## HOL-NanoJava
+
+HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
+
+$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
+  NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
+  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
+  NanoJava/document/root.bib NanoJava/document/root.tex
+	@$(ISATOOL) usedir $(OUT)/HOL NanoJava
 
 ## HOL-CTL
 
@@ -581,7 +591,7 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
+	@rm -f  $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
 		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
 		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
 		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
@@ -589,8 +599,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-MicroJava.gz \
+		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.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 \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \