isabelle: src/FOL/IsaMakefile@61bdf2ae4dc5 (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
9157 998dd2fb5795 new file Provers/make_elim.ML paulson parents: 7355 diff changeset	31	$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
4685 9259feeeb2c8 added clasimp.ML; wenzelm parents: 4518 diff changeset	32	$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
11676 d04e96f8b0fd added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy; wenzelm parents: 9888 diff changeset	33	$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
12526 1b9db2581fe2 mods due to changed 1-point simprocs (quantifier1). nipkow parents: 12370 diff changeset	34	$(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
13550 5a176b8dda84 removal of blast.overloaded paulson parents: 13301 diff changeset	35	FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML IFOL.thy \
11676 d04e96f8b0fd added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy; wenzelm parents: 9888 diff changeset	36	IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
d04e96f8b0fd added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy; wenzelm parents: 9888 diff changeset	37	fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	38	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	39
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	40
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	41	## FOL-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	42
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	43	FOL-ex: FOL $(LOG)/FOL-ex.gz
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	44
14151 b8bb6a6a2c46 converting ex/If to Isar script paulson parents: 13550 diff changeset	45	$(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	46	ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy \
14508 859b11514537 Experimental command for instantiation of locales in proof contexts: ballarin parents: 14236 diff changeset	47	ex/LocaleInst.thy \
12370 f9e6af324d35 added ex/First_Order_Logic.thy, ex/document/root.tex; wenzelm parents: 11771 diff changeset	48	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	49	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	50	ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
2821 b1dcacc4bc26 isatool usedir; wenzelm parents: 2472 diff changeset	51	@$(ISATOOL) usedir $(OUT)/FOL ex
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	52
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	53
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	54	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	55
b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	56	clean:
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	57	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz

author	wenzelm
	Tue, 01 Jun 2004 12:33:50 +0200
changeset 14854	61bdf2ae4dc5
parent 14508	859b11514537
child 15481	fc075ae929e4
permissions	-rw-r--r--