src/Sequents/IsaMakefile
author wenzelm
Sun, 18 Sep 2005 15:20:08 +0200
changeset 17481 75166ebb619b
parent 7098 86583034aacf
child 21426 87ac12bed1ab
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2492
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
     1
#
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
     2
# $Id$
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
     3
#
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
     4
# IsaMakefile for Sequents
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
     5
#
88f15198950f IsaMakefile for Sequents;
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: Sequents
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    10
images: Sequents
6252
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    11
test: Sequents-ILL Sequents-LK Sequents-Modal
4518
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: 2831
diff changeset
    18
OUT = $(ISABELLE_OUTPUT)
4447
b7ee449eb345 log files;
wenzelm
parents: 3505
diff changeset
    19
LOG = $(OUT)/log
2492
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
    20
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    21
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    22
## Sequents
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    23
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    24
Sequents: Pure $(OUT)/Sequents
2492
88f15198950f IsaMakefile for Sequents;
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
2492
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
    28
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6252
diff changeset
    29
$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.ML LK0.thy LK.thy \
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6252
diff changeset
    30
  modal.ML ROOT.ML simpdata.ML S4.ML \
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    31
  S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML
2831
a4f09228b74f isatool usedir;
wenzelm
parents: 2492
diff changeset
    32
	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
2492
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
    33
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    34
6252
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    35
## Sequents-ILL
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    36
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    37
Sequents-ILL: Sequents $(LOG)/Sequents-ILL.gz
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    38
6252
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    39
$(LOG)/Sequents-ILL.gz: $(OUT)/Sequents ILL/ILL_kleene_lemmas.ML \
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    40
  ILL/ILL_predlog.ML ILL/ILL_predlog.thy ILL/ROOT.ML ILL/washing.ML \
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    41
  ILL/washing.thy
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    42
	@$(ISATOOL) usedir $(OUT)/Sequents ILL
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    43
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    44
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    45
## Sequents-LK
2492
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
    46
6252
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    47
Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    48
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    49
$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/hardquant.ML \
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6252
diff changeset
    50
  LK/prop.ML LK/quant.ML LK/Nat.thy LK/Nat.ML
6252
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    51
	@$(ISATOOL) usedir $(OUT)/Sequents LK
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    52
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    53
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    54
## Sequents-Modal
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    55
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    56
Sequents-Modal: Sequents $(LOG)/Sequents-Modal.gz
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    57
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    58
$(LOG)/Sequents-Modal.gz: $(OUT)/Sequents Modal/ROOT.ML \
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    59
  Modal/S43thms.ML Modal/S4thms.ML Modal/Tthms.ML ROOT.ML
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    60
	@$(ISATOOL) usedir $(OUT)/Sequents Modal
2492
88f15198950f IsaMakefile for Sequents;
wenzelm
parents:
diff changeset
    61
4518
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    62
74c01296e818 improved targets;
wenzelm
parents: 4447
diff changeset
    63
## clean
4447
b7ee449eb345 log files;
wenzelm
parents: 3505
diff changeset
    64
b7ee449eb345 log files;
wenzelm
parents: 3505
diff changeset
    65
clean:
6252
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    66
	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ILL.gz \
935f183bf406 examples made separate dirs;
wenzelm
parents: 4518
diff changeset
    67
	  $(LOG)/Sequents-LK.gz $(LOG)/Sequents-Modal.gz