--- a/IsaMakefile	Thu Sep 21 14:15:55 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-
-## 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 slides1.pdf
-
-## Slides
-
-session2: Slides/ROOT2.ML \
-	Slides/document/root* \
-	Slides/Slides2.thy
-	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides
-
-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 slides2.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 
-
-# C&L paper
-
-jour: Journal/*.thy Journal/*.ML 
-	@$(USEDIR) -D generated -f ROOT.ML Prio Journal
-	rm -f Journal/generated/*.aux # otherwise latex will fall over  
-	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
-	cd Journal/generated ; bibtex root
-	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
-	cp Journal/generated/root.pdf journal.pdf 
-
-
-

--- a/README	Thu Sep 21 14:15:55 2017 +0100
+++ b/README	Thu Sep 21 14:23:42 2017 +0100
@@ -3,9 +3,10 @@
 Theories:
 =========
 
+ Graphs.thy              A relational graph library 
+ RTree                   Rooted tree graphs 
  Max.thy                 Some generic facts about Max.
  Precedence_ord.thy      A theory of precedences.
- Moment.thy              The notion of moment.
  PIPDefs.thy             The formal definition of the PIP-model.
  PIPBasics.thy           Basic properties of the PIP-model.
  Correctness.thy         The correctness proof of the PIP-model.
@@ -25,10 +26,10 @@
   Journal:     isabelle build -c -v -d . Journal
   Literature
   
-Test 9
 
 
 
 
 
 
+

--- a/ROOT	Thu Sep 21 14:15:55 2017 +0100
+++ b/ROOT	Thu Sep 21 14:23:42 2017 +0100
@@ -2,7 +2,6 @@
   theories [document = false, quick_and_dirty]
 	"Implementation" 
 	"Correctness"
-        "Test" 
 
 session "Slides2" in "Slides" = PIP +
   options [document_variants="slides2"]

--- a/ROOT.ML	Thu Sep 21 14:15:55 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-use_thy "CpsG"; 
-use_thy "ExtGG";

Binary file journal.pdf has changed

Binary file scripts_structure.pptx has changed