60 $(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated |
60 $(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated |
61 @cp Quotient-Paper/document.pdf qpaper.pdf |
61 @cp Quotient-Paper/document.pdf qpaper.pdf |
62 |
62 |
63 ## Slides |
63 ## Slides |
64 |
64 |
65 session1: Slides/ROOT.ML \ |
65 session1: Slides/ROOT1.ML \ |
66 Slides/document/root* \ |
66 Slides/document/root* \ |
67 Slides/Slides1.thy |
67 Slides/Slides1.thy |
68 @$(USEDIR) -D generated1 -f ROOT.ML HOL-Nominal Slides |
68 @$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides |
69 @perl -i -p -e "s/..isachardoublequoteopen./\\\begin{innerdouble}/g" Sl |
|
70 @perl -i -p -e "s/..isachardoublequoteclose./\\\end{innerdouble}/g" Sli |
|
71 @perl -i -p -e "s/..isacharbackquoteopen./\\\begin{innersingle}/g" Slid |
|
72 @perl -i -p -e "s/..isacharbackquoteclose./\\\end{innersingle}/g" Slide |
|
73 |
69 |
74 slides1: session1 |
70 slides1: session1 |
75 rm -f Slides/generated1/*.aux # otherwise latex will fall over |
71 rm -f Slides/generated1/*.aux # otherwise latex will fall over |
76 cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
72 cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
77 cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
73 cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
78 cp Slides/generated1/root.beamer.pdf Slides/slides.pdf |
74 cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf |
|
75 |
|
76 session2: Slides/ROOT2.ML \ |
|
77 Slides/document/root* \ |
|
78 Slides/Slides2.thy |
|
79 @$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides |
|
80 |
|
81 slides2: session2 |
|
82 rm -f Slides/generated2/*.aux # otherwise latex will fall over |
|
83 cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
84 cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
85 cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf |
|
86 |
|
87 session3: Slides/ROOT3.ML \ |
|
88 Slides/document/root* \ |
|
89 Slides/Slides3.thy |
|
90 @$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides |
|
91 |
|
92 slides3: session3 |
|
93 rm -f Slides/generated3/*.aux # otherwise latex will fall over |
|
94 cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
95 cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
96 cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf |
79 |
97 |
80 slides: slides1 |
98 slides: slides1 |
81 |
99 |
82 |
100 |
83 |
101 |