isabelle: src/FOL/IsaMakefile@adb83939177f (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
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	7	## targets
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	8
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	9	default: FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	10	images: FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	11	test: FOL-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	12	all: images test
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	13
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	14
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	15	## global settings
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	16
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	17	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 2889 diff changeset	18	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	19	LOG = $(OUT)/log
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	20
3233 16a24111ab5a new treatment of Prover files paulson parents: 3118 diff changeset	21
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	22	## FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	23
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	24	FOL: Pure $(OUT)/FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	25
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	26	Pure:
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	27	@cd $(SRC)/Pure; $(ISATOOL) make Pure
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	28
13301 c505fc950cbe added dependency for $(OUT)/Pure kleing parents: 12526 diff changeset	29	$(OUT)/Pure: Pure
c505fc950cbe added dependency for $(OUT)/Pure kleing parents: 12526 diff changeset	30
16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	31	$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	32	$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	33	$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	34	$(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	35	$(SRC)/Provers/make_elim.ML $(SRC)/Provers/quantifier1.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	36	$(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	37	IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	38	document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	39	intprover.ML simpdata.ML
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	40	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	41
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	42
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	43	## FOL-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	44
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	45	FOL-ex: FOL $(LOG)/FOL-ex.gz
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	46
14151 b8bb6a6a2c46 converting ex/If to Isar script paulson parents: 13550 diff changeset	47	$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
12370 f9e6af324d35 added ex/First_Order_Logic.thy, ex/document/root.tex; wenzelm parents: 11771 diff changeset	48	ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy \
15596 8665d08085df First version of global registration command. ballarin parents: 15481 diff changeset	49	ex/LocaleTest.thy \
12370 f9e6af324d35 added ex/First_Order_Logic.thy, ex/document/root.tex; wenzelm parents: 11771 diff changeset	50	ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \
14236 c73d62ce9d1c partial conversion to Isar scripts paulson parents: 14151 diff changeset	51	ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
c73d62ce9d1c partial conversion to Isar scripts paulson parents: 14151 diff changeset	52	ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	53	@$(ISATOOL) usedir $(OUT)/FOL ex
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	54
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	55
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	56	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	57
b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	58	clean:
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	59	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz

author	ballarin
	Wed, 01 Jun 2005 12:30:49 +0200
changeset 16168	adb83939177f
parent 16019	0e1405402d53
child 16831	9ef92b7a2210
permissions	-rw-r--r--