isabelle: src/FOL/IsaMakefile@44cd74a419ce (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 \
41827 98eda7ffde79 setup case_product attribute in HOL and FOL noschinl parents: 40239 diff changeset	32	$(SRC)/Tools/case_product.ML \
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	33	$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	34	$(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	35	$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
27203 9f02853e3f5b removed obsolete ML_SUFFIX; wenzelm parents: 26583 diff changeset	36	$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
30165 6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	37	$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	38	$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
32176 893614e2c35c renamed functor BlastFun to Blast, require explicit theory; wenzelm parents: 30242 diff changeset	39	$(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	40	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	41	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	blanchet
	Thu, 12 May 2011 15:29:19 +0200
changeset 42728	44cd74a419ce
parent 42138	e54a985daa61
child 42793	88bee9f6eec7
permissions	-rw-r--r--