isabelle: src/FOL/IsaMakefile@8f28a91ea135 (annotated)

2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	1	#
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	2	# IsaMakefile for FOL
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	3	#
91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	4
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	5	## targets
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	6
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	7	default: FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	8	images: FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	9	test: FOL-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	10	all: images test
42138 e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; krauss parents: 41827 diff changeset	11	smlnj: all
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	12
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	13
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	14	## global settings
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	15
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	16	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 2889 diff changeset	17	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	18	LOG = $(OUT)/log
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	19
3233 16a24111ab5a new treatment of Prover files paulson parents: 3118 diff changeset	20
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	21	## FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	22
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	23	FOL: Pure $(OUT)/FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	24
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	25	Pure:
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	26	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	27
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	28	$(OUT)/Pure: Pure
13301 c505fc950cbe added dependency for $(OUT)/Pure kleing parents: 12526 diff changeset	29
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	30	$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	31	$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42138 diff changeset	32	$(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42138 diff changeset	33	$(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \
30160 5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 29752 diff changeset	34	$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	35	$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
30165 6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	36	$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	37	$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42138 diff changeset	38	$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \
42799 4e33894aec6d modernized functor names; wenzelm parents: 42793 diff changeset	39	document/root.tex fologic.ML intprover.ML simpdata.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	40	@$(ISABELLE_TOOL) usedir -p 2 -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
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	47	$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \
40239 c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 37134 diff changeset	48	ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
37134 29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 36862 diff changeset	49	ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \
29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 36862 diff changeset	50	ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \
40239 c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 37134 diff changeset	51	ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \
c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 37134 diff changeset	52	ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \
c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 37134 diff changeset	53	ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \
c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 37134 diff changeset	54	ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	55	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	56
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	57
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	58	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	59
b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	60	clean:
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	61	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz

author	huffman
	Wed, 22 Jun 2011 13:45:32 -0700
changeset 43525	8f28a91ea135
parent 42799	4e33894aec6d
child 44121	44adaa6db327
permissions	-rw-r--r--