Theories:
=========
Max.thy Some generic facts about Max.
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 2013-2.
isabelle build -c -v -d . PIP
Othe directories are:
=====================
Slides
Paper
Journal: isabelle build -c -v -d . Journal
Literature
Test 3