wenzelm@2500: #
wenzelm@2500: # $Id$
wenzelm@2500: #
wenzelm@2500: # IsaMakefile for ZF
wenzelm@2500: #
wenzelm@2500: 
wenzelm@2500: #### Base system
wenzelm@2500: 
wenzelm@3118: OUT = $(ISABELLE_OUTPUT)
wenzelm@2500: 
wenzelm@2500: NAMES = ZF upair subset pair domrange \
wenzelm@2500: 	func AC equalities Bool \
wenzelm@2500: 	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
wenzelm@2500: 	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
wenzelm@2500: 	WF Order Ordinal Epsilon Arith Univ \
wenzelm@2500: 	QUniv Datatype OrderArith OrderType \
wenzelm@2500: 	Cardinal CardinalArith Cardinal_AC InfDatatype \
wenzelm@2500: 	Zorn Nat Finite List
wenzelm@2500: 
wenzelm@2500: FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \
wenzelm@2500: 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
wenzelm@2500: 
wenzelm@2500: $(OUT)/ZF: $(OUT)/FOL $(FILES)
wenzelm@3057: 	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
wenzelm@2500: 	@chmod -w $@
wenzelm@2500: 
wenzelm@2500: $(OUT)/FOL:
wenzelm@2500: 	@cd ../FOL; $(ISATOOL) make
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: #### Tests and examples
wenzelm@2500: 
wenzelm@2500: ## IMP-semantics example
wenzelm@2500: 
wenzelm@2500: IMP_NAMES = Com Denotation Equiv
wenzelm@2500: IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
wenzelm@2500: 
wenzelm@2500: IMP: $(OUT)/ZF $(IMP_FILES)
wenzelm@2828: 	@$(ISATOOL) usedir $(OUT)/ZF IMP
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: ## Coinduction example
wenzelm@2500: 
wenzelm@2500: COIND_NAMES = ECR MT Map Static Types Values
wenzelm@2500: 
wenzelm@2500: COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
wenzelm@2500: 	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
wenzelm@2500: 
wenzelm@2500: Coind: $(OUT)/ZF $(COIND_FILES)
wenzelm@2828: 	@$(ISATOOL) usedir $(OUT)/ZF Coind
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: ## AC examples
wenzelm@2500: 
wenzelm@2500: AC_NAMES = AC_Equiv Cardinal_aux \
wenzelm@2500: 	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
wenzelm@2500: 	   DC DC_lemmas HH Hartog WO1_AC \
wenzelm@2500: 	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
wenzelm@2500: 
wenzelm@2500: AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
wenzelm@2500: 	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
wenzelm@2500: 	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
wenzelm@2500: 	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
wenzelm@2500: 
wenzelm@2500: AC: $(OUT)/ZF $(AC_FILES)
wenzelm@2828: 	@$(ISATOOL) usedir $(OUT)/ZF AC
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: ## Residuals example
wenzelm@2500: 
wenzelm@2500: RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
wenzelm@2500: 	      Cube Residuals Terms
wenzelm@2500: 
wenzelm@2500: RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
wenzelm@2500: 
wenzelm@2500: Resid: $(OUT)/ZF $(RESID_FILES)
wenzelm@2828: 	@$(ISATOOL) usedir $(OUT)/ZF Resid
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: ## Miscellaneous examples
wenzelm@2500: 
wenzelm@2500: EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
wenzelm@2500: 	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit
wenzelm@2500: 
wenzelm@2500: EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
wenzelm@2500: 
wenzelm@2500: ex: $(OUT)/ZF $(EX_FILES)
wenzelm@2828: 	@$(ISATOOL) usedir $(OUT)/ZF ex
wenzelm@2500: 
wenzelm@2500: 
wenzelm@2500: ## Full test
wenzelm@2500: 
wenzelm@2500: test: $(OUT)/ZF IMP Coind AC Resid ex
wenzelm@2500: 	echo 'Test examples ran successfully' > test
wenzelm@2500: 
wenzelm@2500: .PRECIOUS: $(OUT)/FOL $(OUT)/ZF