| author | wu | 
| Mon, 13 Aug 2012 10:37:37 +0000 | |
| changeset 363 | c89f82fb95f8 | 
| parent 334 | d47c2143ab8a | 
| child 367 | 79401279ba21 | 
| permissions | -rw-r--r-- | 
| 16 | 1  | 
|
2  | 
## targets  | 
|
3  | 
||
| 
334
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
4  | 
default: slides4  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
5  | 
all: slides itp  | 
| 16 | 6  | 
|
7  | 
## global settings  | 
|
8  | 
||
9  | 
SRC = $(ISABELLE_HOME)/src  | 
|
10  | 
OUT = $(ISABELLE_OUTPUT)  | 
|
11  | 
LOG = $(OUT)/log  | 
|
12  | 
||
13  | 
||
14  | 
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true  | 
|
| 24 | 15  | 
|
16  | 
||
| 333 | 17  | 
## Slides 1  | 
| 16 | 18  | 
|
| 24 | 19  | 
session1: Slides/ROOT.ML \  | 
| 16 | 20  | 
Slides/document/root* \  | 
| 24 | 21  | 
Slides/Slides.thy  | 
| 203 | 22  | 
@$(USEDIR) -D generated -f ROOT.ML HOL Slides  | 
| 24 | 23  | 
|
| 333 | 24  | 
slides1: session1  | 
| 24 | 25  | 
rm -f Slides/generated/*.aux # otherwise latex will fall over  | 
26  | 
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex  | 
|
27  | 
cp Slides/generated/root.beamer.pdf Slides/slides.pdf  | 
|
28  | 
||
| 333 | 29  | 
## Slides 2  | 
| 203 | 30  | 
|
| 333 | 31  | 
session2: Slides/ROOT.ML \  | 
| 203 | 32  | 
Slides/document/root* \  | 
33  | 
Slides/Slides1.thy  | 
|
34  | 
@$(USEDIR) -D generated -f ROOT1.ML HOL Slides  | 
|
35  | 
||
| 333 | 36  | 
slides2: session2  | 
| 203 | 37  | 
rm -f Slides/generated/*.aux # otherwise latex will fall over  | 
38  | 
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex  | 
|
39  | 
cp Slides/generated/root.beamer.pdf Slides/slides1.pdf  | 
|
40  | 
||
| 333 | 41  | 
## Slides 3  | 
| 258 | 42  | 
|
| 333 | 43  | 
session3: Slides/ROOT.ML \  | 
| 258 | 44  | 
Slides/document/root* \  | 
45  | 
Slides/Slides2.thy  | 
|
46  | 
@$(USEDIR) -D generated -f ROOT2.ML HOL Slides  | 
|
47  | 
||
| 333 | 48  | 
slides3: session3  | 
| 258 | 49  | 
rm -f Slides/generated/*.aux # otherwise latex will fall over  | 
50  | 
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex  | 
|
51  | 
cp Slides/generated/root.beamer.pdf Slides/slides2.pdf  | 
|
| 16 | 52  | 
|
| 
334
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
53  | 
## Slides 4  | 
| 16 | 54  | 
|
| 
334
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
55  | 
session4: Slides/ROOT.ML \  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
56  | 
Slides/document/root* \  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
57  | 
Slides/Slides2.thy  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
58  | 
@$(USEDIR) -D generated -f ROOT4.ML HOL Slides  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
59  | 
|
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
60  | 
slides4: session4  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
61  | 
rm -f Slides/generated/*.aux # otherwise latex will fall over  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
62  | 
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
63  | 
cp Slides/generated/root.beamer.pdf Slides/slides4.pdf  | 
| 72 | 64  | 
|
| 16 | 65  | 
|
| 
334
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
66  | 
slides: slides1 slides2 slides3 slides4  | 
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
67  | 
|
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
68  | 
|
| 
 
d47c2143ab8a
partially updated conference paper; slightly tuned journal paper
 
urbanc 
parents: 
333 
diff
changeset
 | 
69  | 
## ITP itp  | 
| 
36
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
70  | 
|
| 333 | 71  | 
session_itp: Paper/ROOT.ML \  | 
| 
36
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
72  | 
Paper/document/root* \  | 
| 
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
73  | 
Paper/*.thy  | 
| 
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
74  | 
@$(USEDIR) -D generated -f ROOT.ML HOL Paper  | 
| 
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
75  | 
|
| 333 | 76  | 
itp: session_itp  | 
| 
36
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
77  | 
rm -f Paper/generated/*.aux # otherwise latex will fall over  | 
| 
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
78  | 
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex  | 
| 66 | 79  | 
cd Paper/generated ; bibtex root  | 
| 
36
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
80  | 
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex  | 
| 
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
81  | 
cp Paper/generated/root.pdf paper.pdf  | 
| 
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
82  | 
|
| 
162
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
83  | 
## Journal Version  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
84  | 
|
| 333 | 85  | 
session_journal: Journal/ROOT.ML \  | 
| 
162
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
86  | 
Journal/document/root* \  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
87  | 
Journal/*.thy  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
88  | 
@$(USEDIR) -D generated -f ROOT.ML HOL Journal  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
89  | 
|
| 333 | 90  | 
journal: session_journal  | 
| 
162
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
91  | 
rm -f Journal/generated/*.aux # otherwise latex will fall over  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
92  | 
cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
93  | 
cd Journal/generated ; bibtex root  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
94  | 
cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
95  | 
cp Journal/generated/root.pdf journal.pdf  | 
| 
 
e93760534354
added directory for journal version; took uptodate version of the theory files
 
urbanc 
parents: 
72 
diff
changeset
 | 
96  | 
|
| 
36
 
f5cc33a0ba99
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
 
wu 
parents: 
31 
diff
changeset
 | 
97  | 
|
| 16 | 98  | 
## clean  | 
99  | 
||
100  | 
clean:  | 
|
| 333 | 101  | 
rm -rf Slides/generated*  | 
102  | 
rm -rf Paper/generated*  | 
|
103  | 
rm -rf Journal/generated*  |