597
+ − 1
+ − 2
## targets
+ − 3
+ − 4
default: Quot
+ − 5
images:
+ − 6
601
+ − 7
all: Quot
597
+ − 8
+ − 9
+ − 10
## global settings
+ − 11
+ − 12
SRC = $(ISABELLE_HOME)/src
+ − 13
OUT = $(ISABELLE_OUTPUT)
+ − 14
LOG = $(OUT)/log
+ − 15
757
+ − 16
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ##-D generated
+ − 17
597
+ − 18
+ − 19
## Quot
+ − 20
+ − 21
Quot: $(LOG)/HOL-Quot.gz
+ − 22
+ − 23
$(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy
1460
+ − 24
@$(USEDIR) HOL-Plain Quot
754
+ − 25
+ − 26
paper: $(LOG)/HOL-Quot-Paper.gz
+ − 27
+ − 28
$(LOG)/HOL-Quot-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
757
+ − 29
@$(USEDIR) -D generated HOL Paper
754
+ − 30
$(ISATOOL) document -o pdf Paper/generated
+ − 31
@cp Paper/document.pdf paper.pdf
597
+ − 32
764
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
keywords:
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
mkdir -p tmp
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/Pure.gz tmp
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36
cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/HOL.gz tmp
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/Pure-ProofGeneral.gz tmp
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/HOL-Nominal.gz tmp
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
cp $(LOG)/HOL-Nominal-Quot.gz tmp
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
isabelle keywords -k quot tmp/*
1460
+ − 41
597
+ − 42
## clean
+ − 43
+ − 44
clean:
+ − 45
@rm -f $(LOG)/HOL-Quot.gz