author | blanchet |
Mon, 20 Sep 2010 17:12:52 +0200 (2010-09-20) | |
changeset 39562 | be44a81ca5ab |
parent 37134 | 29bd6c2ffba8 |
child 40239 | c4336e45f199 |
permissions | -rw-r--r-- |
2433 | 1 |
# |
2 |
# IsaMakefile for FOL |
|
3 |
# |
|
4 |
||
4518 | 5 |
## targets |
6 |
||
7 |
default: FOL |
|
8 |
images: FOL |
|
9 |
test: FOL-ex |
|
10 |
all: images test |
|
11 |
||
12 |
||
13 |
## global settings |
|
14 |
||
15 |
SRC = $(ISABELLE_HOME)/src |
|
3118 | 16 |
OUT = $(ISABELLE_OUTPUT) |
4447 | 17 |
LOG = $(OUT)/log |
2433 | 18 |
|
3233 | 19 |
|
4518 | 20 |
## FOL |
21 |
||
27203 | 22 |
FOL: Pure $(OUT)/FOL |
2433 | 23 |
|
4518 | 24 |
Pure: |
28500 | 25 |
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure |
2433 | 26 |
|
27203 | 27 |
$(OUT)/Pure: Pure |
13301 | 28 |
|
27203 | 29 |
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ |
16019 | 30 |
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
27203 | 31 |
$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \ |
32 |
$(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
|
33 |
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \ |
27203 | 34 |
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ |
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset
|
35 |
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \ |
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset
|
36 |
$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
30242
diff
changeset
|
37 |
$(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
|
38 |
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
|
39 |
simpdata.ML |
28500 | 40 |
@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL |
2433 | 41 |
|
4518 | 42 |
|
43 |
## FOL-ex |
|
44 |
||
45 |
FOL-ex: FOL $(LOG)/FOL-ex.gz |
|
2433 | 46 |
|
27203 | 47 |
$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ |
29752 | 48 |
ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \ |
37134 | 49 |
ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \ |
50 |
ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \ |
|
51 |
ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML \ |
|
29752 | 52 |
ex/Classical.thy ex/document/root.tex ex/Foundation.thy \ |
53 |
ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy \ |
|
54 |
ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \ |
|
55 |
ex/Quantifiers_Cla.thy |
|
28500 | 56 |
@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex |
2433 | 57 |
|
4518 | 58 |
|
59 |
## clean |
|
4447 | 60 |
|
61 |
clean: |
|
27203 | 62 |
@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz |