src/HOL/IsaMakefile
changeset 19497 630073ef9212
parent 19404 9bf2cdc9e8e8
child 19499 1a082c1257d7
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 28 15:58:30 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 28 15:59:31 2006 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
     1.7 -images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA HOL4
     1.8 +images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal TLA HOL4
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library)
    1.11  test: \
    1.12 @@ -30,6 +30,7 @@
    1.13    HOL-MicroJava \
    1.14    HOL-Modelcheck \
    1.15    HOL-NanoJava \
    1.16 +  HOL-Nominal-Examples \
    1.17    HOL-NumberTheory \
    1.18    HOL-Prolog \
    1.19    HOL-SET-Protocol \
    1.20 @@ -725,10 +726,32 @@
    1.21  	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
    1.22  
    1.23  
    1.24 +## HOL-Nominal
    1.25 +
    1.26 +HOL-Nominal: HOL $(OUT)/HOL-Nominal
    1.27 +
    1.28 +$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML Nominal/Nominal.thy		\
    1.29 +  Nominal/nominal_atoms.ML Nominal/nominal_induct.ML				\
    1.30 +  Nominal/nominal_package.ML Nominal/nominal_permeq.ML
    1.31 +	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
    1.32 +
    1.33 +
    1.34 +## HOL-Nominal-Examples
    1.35 +
    1.36 +HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
    1.37 +
    1.38 +$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy	\
    1.39 +  Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy 				\
    1.40 +  Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy		\
    1.41 +  Nominal/Examples/Recursion.thy Nominal/Examples/SN.thy			\
    1.42 +  Nominal/Examples/Weakening.thy
    1.43 +	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
    1.44 +
    1.45 +
    1.46  ## clean
    1.47  
    1.48  clean:
    1.49 -	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/TLA \
    1.50 +	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
    1.51  		$(LOG)/HOL.gz $(LOG)/TLA.gz \
    1.52  		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
    1.53  		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
    1.54 @@ -739,6 +762,7 @@
    1.55  		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.56                  $(LOG)/HOL-Bali.gz \
    1.57  		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
    1.58 +                $(LOG)/HOL-Nominal-Examples.gz \
    1.59  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
    1.60  		$(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
    1.61  		$(LOG)/HOL-Complex.gz \