README
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 06 Dec 2012 15:11:21 +0000
changeset 0 110247f9d47e
child 29 408ff78ce28f
permissions -rw-r--r--
added
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
Theories:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
=========
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
 Precedence_ord.thy      A theory of precedences.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
 Moment.thy              The notion of moment.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
 PrioGDef.thy            The formal definition of the PIP-model.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
 PrioG.thy               Basic properties of the PIP-model.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
 ExtGG.thy               The correctness proof of the PIP-model.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
 CpsG.thy                Properties interesting for an implementation.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
The repository can be checked using Isabelle 2011-1.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
  isabelle make session
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14