1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
#=====================================================================
# Makefile for typesetting the HOL course slides.
# =====================================================================
default:
@echo "Type \"make all\" to typeset the HOL course slides"
intro.dvi: intro.tex
latex intro.tex
logicA.dvi: logicA.tex
latex logicA.tex
logicB.dvi: logicB.tex
latex logicB.tex
macros.dvi: macros.tex
latex macros.tex
ml.dvi: ml.tex
latex ml.tex
primrec.dvi: primrec.tex
latex primrec.tex
systemA.dvi: systemA.tex
latex systemA.tex
systemB.dvi: systemB.tex
latex systemB.tex
thmproveA.dvi: thmproveA.tex
latex thmproveA.tex
thmproveB.dvi: thmproveB.tex
latex thmproveB.tex
tydefs.dvi: tydefs.tex
latex tydefs.tex
all: intro.dvi logicA.dvi logicB.dvi ml.dvi primrec.dvi systemA.dvi\
systemB.dvi thmproveA.dvi thmproveB.dvi tydefs.dvi
echo "course made"
|
