isabelle: src/FOL/IsaMakefile@df8448bc7a8b (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
17821 daffb154f73e ML_SUFFIX in targets (experimental); wenzelm parents: 16831 diff changeset	24	FOL: Pure $(OUT)/FOL$(ML_SUFFIX)
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
17821 daffb154f73e ML_SUFFIX in targets (experimental); wenzelm parents: 16831 diff changeset	29	$(OUT)/Pure$(ML_SUFFIX): Pure
13301 c505fc950cbe added dependency for $(OUT)/Pure kleing parents: 12526 diff changeset	30
18482 ac8456b4080c added Provers/project_rule.ML wenzelm parents: 18203 diff changeset	31	$(OUT)/FOL$(ML_SUFFIX): $(OUT)/Pure$(ML_SUFFIX) $(SRC)/Provers/blast.ML \
16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	32	$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
23171 861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 22822 diff changeset	33	$(SRC)/Tools/IsaPlanner/zipper.ML \
861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 22822 diff changeset	34	$(SRC)/Tools/IsaPlanner/isand.ML \
861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 22822 diff changeset	35	$(SRC)/Tools/IsaPlanner/rw_tools.ML \
861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 22822 diff changeset	36	$(SRC)/Tools/IsaPlanner/rw_inst.ML \
16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	37	$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
24830 a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML; wenzelm parents: 23914 diff changeset	38	$(SRC)/Tools/induct.ML \
18529 540da2415751 removed obsolete Provers/make_elim.ML; wenzelm parents: 18482 diff changeset	39	$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
21539 c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 19839 diff changeset	40	$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML \
18596 1e876583e247 removed obsolete eqrule_FOL_data.ML; wenzelm parents: 18529 diff changeset	41	document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
18203 9bd26bda96ef FOL: -p 2; wenzelm parents: 17821 diff changeset	42	@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	43
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	44
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	45	## FOL-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	46
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	47	FOL-ex: FOL $(LOG)/FOL-ex.gz
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	48
17821 daffb154f73e ML_SUFFIX in targets (experimental); wenzelm parents: 16831 diff changeset	49	$(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \
22822 c1a6a2159e69 removed obsolete induct/simp tactic; wenzelm parents: 21539 diff changeset	50	ex/If.thy ex/IffOracle.thy ex/LocaleTest.thy \
c1a6a2159e69 removed obsolete induct/simp tactic; wenzelm parents: 21539 diff changeset	51	ex/Nat.thy ex/Natural_Numbers.thy ex/Miniscope.thy \
19820 0d7564c798d0 removed obsolete ML files; wenzelm parents: 19819 diff changeset	52	ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex \
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23171 diff changeset	53	ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy \
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23171 diff changeset	54	ex/Propositional_Int.thy ex/Propositional_Cla.thy \
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23171 diff changeset	55	ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	56	@$(ISATOOL) usedir $(OUT)/FOL ex
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	57
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	58
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	59	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	60
b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	61	clean:
17821 daffb154f73e ML_SUFFIX in targets (experimental); wenzelm parents: 16831 diff changeset	62	@rm -f $(OUT)/FOL$(ML_SUFFIX) $(LOG)/FOL.gz $(LOG)/FOL-ex.gz

author	haftmann
	Thu, 04 Oct 2007 19:41:55 +0200
changeset 24841	df8448bc7a8b
parent 24830	a7b3ab44d993
child 26583	9f81ab1b7b64
permissions	-rw-r--r--