src/FOL/IsaMakefile
author paulson
Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255 38f96394c099
parent 7355 4c43090659ca
child 9157 998dd2fb5795
permissions -rw-r--r--
new distributive laws
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
# $Id$
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
     3
#
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
     4
# IsaMakefile for FOL
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
     5
#
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
     6
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
     7
## targets
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
     8
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
     9
default: FOL
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    10
images: FOL
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    11
test: FOL-ex
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    12
all: images test
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
74c01296e818 improved targets;
wenzelm
parents: 4447
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:
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    27
	@cd $(SRC)/Pure; $(ISATOOL) make Pure
2433
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
    28
4685
9259feeeb2c8 added clasimp.ML;
wenzelm
parents: 4518
diff changeset
    29
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	\
9259feeeb2c8 added clasimp.ML;
wenzelm
parents: 4518
diff changeset
    30
  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
9259feeeb2c8 added clasimp.ML;
wenzelm
parents: 4518
diff changeset
    31
  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML \
9259feeeb2c8 added clasimp.ML;
wenzelm
parents: 4518
diff changeset
    32
  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML FOL.ML \
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 4685
diff changeset
    33
  FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 4685
diff changeset
    34
  IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML fologic.ML \
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 4685
diff changeset
    35
  hypsubstdata.ML intprover.ML simpdata.ML
2821
b1dcacc4bc26 isatool usedir;
wenzelm
parents: 2472
diff changeset
    36
	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
2433
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
    37
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    38
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    39
## FOL-ex
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    40
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    41
FOL-ex: FOL $(LOG)/FOL-ex.gz
2433
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
    42
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    43
$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/If.ML ex/If.thy ex/IffOracle.ML \
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    44
  ex/IffOracle.thy ex/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy \
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    45
  ex/Nat2.ML ex/Nat2.thy ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML \
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    46
  ex/foundn.ML ex/int.ML ex/intro.ML ex/prop.ML ex/quant.ML
2821
b1dcacc4bc26 isatool usedir;
wenzelm
parents: 2472
diff changeset
    47
	@$(ISATOOL) usedir $(OUT)/FOL ex
2433
91016075afe8 IsaMakefile for FOL;
wenzelm
parents:
diff changeset
    48
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    49
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    50
## clean
4447
b7ee449eb345 log files;
wenzelm
parents: 4349
diff changeset
    51
b7ee449eb345 log files;
wenzelm
parents: 4349
diff changeset
    52
clean:
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    53
	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz