README
author zhangx
Thu, 28 Jan 2016 21:14:17 +0800 (2016-01-28)
changeset 90 ed938e2246b9
parent 83 61a4429e7d4d
child 146 2d66c0b0bacf
permissions -rw-r--r--
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 . PIP


Othe directories are:
=====================

  Slides
  Paper
  Journal:     isabelle build -c -v -d . Journal
  Literature
  
Test 3