isabelle: src/FOL/IsaMakefile@93eda35a8377 (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
45860 93eda35a8377 more visible benchmarks; wenzelm parents: 44121 diff changeset	11	full: all
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	12	smlnj: all
4518 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
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 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:
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	27	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	28
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	29	$(OUT)/Pure: Pure
13301 c505fc950cbe added dependency for $(OUT)/Pure kleing parents: 12526 diff changeset	30
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	31	$(OUT)/FOL: $(OUT)/Pure $(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 \
44121 44adaa6db327 old term operations are legacy; wenzelm parents: 42799 diff changeset	33	$(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML \
44adaa6db327 old term operations are legacy; wenzelm parents: 42799 diff changeset	34	$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
44adaa6db327 old term operations are legacy; wenzelm parents: 42799 diff changeset	35	$(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	36	$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	37	$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
30165 6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	38	$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	39	$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42138 diff changeset	40	$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \
42799 4e33894aec6d modernized functor names; wenzelm parents: 42793 diff changeset	41	document/root.tex fologic.ML intprover.ML simpdata.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	42	@$(ISABELLE_TOOL) 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
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	49	$(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	50	ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
37134 29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 36862 diff changeset	51	ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \
29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 36862 diff changeset	52	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	53	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	54	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	55	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	56	ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	57	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	58
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	59
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	60	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	61
b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	62	clean:
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	63	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz

author	wenzelm
	Wed, 14 Dec 2011 12:02:02 +0100
changeset 45860	93eda35a8377
parent 44121	44adaa6db327
permissions	-rw-r--r--