isabelle: src/FOL/IsaMakefile@524bb42442dc (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
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	11
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	12
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	13	## global settings
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	14
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	15	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 2889 diff changeset	16	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4349 diff changeset	17	LOG = $(OUT)/log
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	18
3233 16a24111ab5a new treatment of Prover files paulson parents: 3118 diff changeset	19
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	20	## FOL
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	21
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	22	FOL: Pure $(OUT)/FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	23
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	24	Pure:
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	25	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	26
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	27	$(OUT)/Pure: Pure
13301 c505fc950cbe added dependency for $(OUT)/Pure kleing parents: 12526 diff changeset	28
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	29	$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15596 diff changeset	30	$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
41827 98eda7ffde79 setup case_product attribute in HOL and FOL noschinl parents: 40239 diff changeset	31	$(SRC)/Tools/case_product.ML \
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	32	$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	33	$(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 \
32176 893614e2c35c renamed functor BlastFun to Blast, require explicit theory; wenzelm parents: 30242 diff changeset	38	$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML \
893614e2c35c renamed functor BlastFun to Blast, require explicit theory; wenzelm parents: 30242 diff changeset	39	document/root.tex fologic.ML hypsubstdata.ML intprover.ML \
30165 6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	40	simpdata.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	41	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	42
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	43
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	44	## FOL-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	45
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	46	FOL-ex: FOL $(LOG)/FOL-ex.gz
2433 91016075afe8 IsaMakefile for FOL; wenzelm parents: diff changeset	47
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	48	$(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	49	ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
37134 29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 36862 diff changeset	50	ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \
29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 36862 diff changeset	51	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	52	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	53	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	54	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	55	ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27203 diff changeset	56	@$(ISABELLE_TOOL) 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:
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	62	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz

author	wenzelm
	Sat, 26 Mar 2011 15:55:22 +0100
changeset 42122	524bb42442dc
parent 41827	98eda7ffde79
child 42138	e54a985daa61
permissions	-rw-r--r--