Theories:========= Precedence_ord.thy A theory of precedences. Moment.thy The notion of moment. PrioGDef.thy The formal definition of the PIP-model. PrioG.thy Basic properties of the PIP-model. ExtGG.thy The correctness proof of the PIP-model. CpsG.thy Properties interesting for an implementation.The repository can be checked using Isabelle 2011-1. isabelle make session