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. 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. Implementation.thy Properties interesting for an implementation.The repository can be checked using Isabelle 2016-1. isabelle build -c -v -d . PIPOthe directories are:===================== Slides Paper Journal: isabelle build -c -v -d . Journal Literature