# HG changeset patch # User urbanc # Date 1346245546 0 # Node ID 79401279ba21c902453cb2c30406d873563f1755 # Parent 827e487b9e924c0ce10489e4b05eff1bee10cb79 for slides diff -r 827e487b9e92 -r 79401279ba21 IsaMakefile --- a/IsaMakefile Wed Aug 29 13:05:25 2012 +0000 +++ b/IsaMakefile Wed Aug 29 13:05:46 2012 +0000 @@ -24,7 +24,7 @@ slides1: session1 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated/root.beamer.pdf Slides/slides.pdf + cp Slides/generated/root.beamer.pdf Slides/slides1.pdf ## Slides 2 @@ -36,7 +36,7 @@ slides2: session2 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated/root.beamer.pdf Slides/slides1.pdf + cp Slides/generated/root.beamer.pdf Slides/slides2.pdf ## Slides 3 @@ -48,13 +48,13 @@ slides3: session3 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated/root.beamer.pdf Slides/slides2.pdf + cp Slides/generated/root.beamer.pdf Slides/slides3.pdf ## Slides 4 session4: Slides/ROOT.ML \ Slides/document/root* \ - Slides/Slides2.thy + Slides/Slides4.thy @$(USEDIR) -D generated -f ROOT4.ML HOL Slides slides4: session4 @@ -62,8 +62,21 @@ cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated/root.beamer.pdf Slides/slides4.pdf +## Slides 5 -slides: slides1 slides2 slides3 slides4 +session5: Slides/ROOT.ML \ + Slides/document/root* \ + Slides/Slides5.thy + @$(USEDIR) -D generated -f ROOT5.ML HOL Slides + +slides5: session5 + rm -f Slides/generated/*.aux # otherwise latex will fall over + cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated/root.beamer.pdf Slides/slides5.pdf + + + +slides: slides1 slides2 slides3 slides4 slides5 ## ITP itp