Retrofiting of:
CpsG.thy (the parallel copy of PIPBasics.thy),
ExtGG.thy (The paralell copy of Implemenation.thy),
PrioG.thy (The paralell copy of Correctness.thy)
has completed.
The next step is to overwite original copies with the paralell ones.
Theories:========= 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. Implementation.thy Properties interesting for an implementation.The repository can be checked using Isabelle 2013-2. isabelle build -c -v -d . PIPOthe directories are:===================== Slides Paper Journal: isabelle build -c -v -d . Journal LiteratureTest 3