# HG changeset patch
# User berghofe
# Date 1146232771 -7200
# Node ID 630073ef9212b5a16bfa6882825becb0bcc4a3e7
# Parent  79dbe35c6cbaeb042eb16b26c7748b29c889e650
Added new targets for nominal datatype package.

diff -r 79dbe35c6cba -r 630073ef9212 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 28 15:58:30 2006 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 28 15:59:31 2006 +0200
@@ -6,7 +6,7 @@
 
 default: HOL
 generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
-images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA HOL4
+images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal TLA HOL4
 
 #Note: keep targets sorted (except for HOL-Library)
 test: \
@@ -30,6 +30,7 @@
   HOL-MicroJava \
   HOL-Modelcheck \
   HOL-NanoJava \
+  HOL-Nominal-Examples \
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-SET-Protocol \
@@ -725,10 +726,32 @@
 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
 
 
+## HOL-Nominal
+
+HOL-Nominal: HOL $(OUT)/HOL-Nominal
+
+$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML Nominal/Nominal.thy		\
+  Nominal/nominal_atoms.ML Nominal/nominal_induct.ML				\
+  Nominal/nominal_package.ML Nominal/nominal_permeq.ML
+	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
+
+
+## HOL-Nominal-Examples
+
+HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
+
+$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy	\
+  Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy 				\
+  Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy		\
+  Nominal/Examples/Recursion.thy Nominal/Examples/SN.thy			\
+  Nominal/Examples/Weakening.thy
+	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
+
+
 ## clean
 
 clean:
-	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/TLA \
+	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
 		$(LOG)/HOL.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 \
@@ -739,6 +762,7 @@
 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
                 $(LOG)/HOL-Bali.gz \
 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
+                $(LOG)/HOL-Nominal-Examples.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
 		$(LOG)/HOL-Complex.gz \