author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Tue, 03 Jun 2014 15:00:12 +0100 | |
changeset 40 | 0781a2fc93f1 |
parent 35 | 92f61f6a0fe7 |
child 45 | fc83f79009bd |
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 |
|
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
29
diff
changeset
|
4 |
Max.thy Some generic facts about Max. |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
Precedence_ord.thy A theory of precedences. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
Moment.thy The notion of moment. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
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
|
8 |
PrioG.thy Basic properties of the PIP-model. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
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
|
10 |
CpsG.thy Properties interesting for an implementation. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
|
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
29
diff
changeset
|
12 |
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
13 |
The repository can be checked using Isabelle 2013-2. |
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
14 |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
15 |
isabelle build -d . PIP |
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
16 |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
17 |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
18 |
Othe directories are: |
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
19 |
===================== |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
21 |
Slides |
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
22 |
Paper |
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
23 |
Journal |
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
24 |
Literature |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
26 |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
27 |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
28 |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
29 |