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