src/FOL/IsaMakefile
author blanchet
Tue, 15 Nov 2011 22:13:39 +0100
changeset 45509 624872fc47bf
parent 44121 44adaa6db327
child 45860 93eda35a8377
permissions -rw-r--r--
use consts, not frees, for lambda-lifting
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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			\
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42799
diff changeset
    32
  $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML		\
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42799
diff changeset
    33
  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42799
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		\
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42138
diff changeset
    39
  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
42799
4e33894aec6d modernized functor names;
wenzelm
parents: 42793
diff changeset
    40
  document/root.tex fologic.ML intprover.ML 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