diff -r c4783e4ef43f -r a04084de4946 IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IsaMakefile	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,51 @@
+
+## targets
+
+default: itp
+all: session itp slides1
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+
+USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
+
+
+## Slides
+
+session1: Slides/ROOT1.ML \
+	Slides/document/root* \
+	Slides/Slides1.thy
+	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
+
+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
+
+# main files                        
+
+session: ./ROOT.ML ./*.thy
+	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
+
+
+# itp paper
+
+itp: Paper/*.thy Paper/*.ML 
+	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
+	rm -f Paper/generated/*.aux # otherwise latex will fall over  
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
+	cd Paper/generated ; bibtex root
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	cp Paper/generated/root.pdf paper.pdf 
+
+
+slides: Slides/ROOT1.ML Slides/*.thy 
+	@$(USEDIR) -D generated -f ROOT1.ML Prio Slides
+	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
+