equal
deleted
inserted
replaced
58 $(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy |
58 $(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy |
59 @$(USEDIR) -D generated HOL Quotient-Paper |
59 @$(USEDIR) -D generated HOL Quotient-Paper |
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 |
|
64 |
|
65 session1: Slides/ROOT.ML \ |
|
66 Slides/document/root* \ |
|
67 Slides/Slides1.thy |
|
68 @$(USEDIR) -D generated1 -f ROOT.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 |
|
74 slides1: session1 |
|
75 rm -f Slides/generated1/*.aux # otherwise latex will fall over |
|
76 cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
77 cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
78 cp Slides/generated1/root.beamer.pdf Slides/slides.pdf |
|
79 |
|
80 slides: slides1 |
|
81 |
|
82 |
|
83 |
63 |
84 |
64 ## clean |
85 ## clean |
65 |
86 |
66 clean: |
87 clean: |
67 @rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz |
88 @rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz |