isabelle: src/FOL/IsaMakefile@50403e5a44c0 (annotated)

2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	1	#
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	2	# $Id$
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	3	#
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	4	# IsaMakefile for FOL
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	5	#
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	6
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 2889 diff changeset	7	OUT = $(ISABELLE_OUTPUT)
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	8
3233 16a24111ab5a new treatment of Prover files paulson parents: 3118 diff changeset	9	PROVERS = hypsubst.ML classical.ML blast.ML \
16a24111ab5a new treatment of Prover files paulson parents: 3118 diff changeset	10	simplifier.ML splitter.ML ind.ML
16a24111ab5a new treatment of Prover files paulson parents: 3118 diff changeset	11
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	12	FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
4349 50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL paulson parents: 3817 diff changeset	13	fologic.ML cladata.ML $(PROVERS:%=../Provers/%)
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	14
3817 f20f193d42b4 removed declIffOracle; wenzelm parents: 3612 diff changeset	15	EX_NAMES = If List Nat Nat2 Prolog IffOracle
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	16	EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	17	ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	18
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	19
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	20	$(OUT)/FOL: $(OUT)/Pure $(FILES)
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	21	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	22
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	23	$(OUT)/Pure:
2472 e5b407ff3100 minor tuning; wenzelm parents: 2433 diff changeset	24	@cd ../Pure; $(ISATOOL) make
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	25
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	26	test: ex/ROOT.ML $(OUT)/FOL $(EX_FILES)
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	27	@$(ISATOOL) usedir $(OUT)/FOL ex
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	28
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	29	.PRECIOUS: $(OUT)/Pure $(OUT)/FOL

author	paulson
	Wed, 03 Dec 1997 10:48:16 +0100
changeset 4349	50403e5a44c0
parent 3817	f20f193d42b4
child 4447	b7ee449eb345
permissions	-rw-r--r--