README
changeset 64 b4bcd1edbb6d
parent 52 78adeef368c1
child 83 61a4429e7d4d
equal deleted inserted replaced
63:b620a2a0806a 64:b4bcd1edbb6d
     2 =========
     2 =========
     3 
     3 
     4  Max.thy                 Some generic facts about Max.
     4  Max.thy                 Some generic facts about Max.
     5  Precedence_ord.thy      A theory of precedences.
     5  Precedence_ord.thy      A theory of precedences.
     6  Moment.thy              The notion of moment.
     6  Moment.thy              The notion of moment.
     7  PrioGDef.thy            The formal definition of the PIP-model.
     7  PIPDefs.thy             The formal definition of the PIP-model.
     8  PrioG.thy               Basic properties of the PIP-model.
     8  PIPBasics.thy           Basic properties of the PIP-model.
     9  ExtGG.thy               The correctness proof of the PIP-model.
     9  Correctness.thy         The correctness proof of the PIP-model.
    10  CpsG.thy                Properties interesting for an implementation.
    10  Implementation.thy      Properties interesting for an implementation.
    11 
    11 
    12 
    12 
    13 The repository can be checked using Isabelle 2013-2.
    13 The repository can be checked using Isabelle 2013-2.
    14 
    14 
    15   isabelle build -c -v -d . PIP
    15   isabelle build -c -v -d . PIP