| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 11 Apr 2017 03:03:33 +0800 | |
| changeset 158 | 2bb3b65fc99f |
| parent 151 | a79a6a286108 |
| child 195 | 6b26b1fd4da5 |
| permissions | -rw-r--r-- |
| 146 | 1 |
|
2 |
||
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
Theories: |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
========= |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
|
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
|
6 |
Max.thy Some generic facts about Max. |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
Precedence_ord.thy A theory of precedences. |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
Moment.thy The notion of moment. |
|
64
b4bcd1edbb6d
renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
52
diff
changeset
|
9 |
PIPDefs.thy The formal definition of the PIP-model. |
|
b4bcd1edbb6d
renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
52
diff
changeset
|
10 |
PIPBasics.thy Basic properties of the PIP-model. |
|
b4bcd1edbb6d
renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
52
diff
changeset
|
11 |
Correctness.thy The correctness proof of the PIP-model. |
|
b4bcd1edbb6d
renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
52
diff
changeset
|
12 |
Implementation.thy Properties interesting for an implementation. |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
|
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
15 |
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
|
16 |
|
|
45
fc83f79009bd
updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
35
diff
changeset
|
17 |
isabelle build -c -v -d . PIP |
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
18 |
|
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
19 |
|
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
20 |
Othe directories are: |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
21 |
===================== |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
|
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
23 |
Slides |
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
24 |
Paper |
|
50
38ad30559775
test
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
47
diff
changeset
|
25 |
Journal: isabelle build -c -v -d . Journal |
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
26 |
Literature |
| 47 | 27 |
|
| 151 | 28 |
Test 9 |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
|
|
29
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
30 |
|
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
31 |
|
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
32 |
|
|
408ff78ce28f
updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
33 |
|
|
30
7f87232d9424
test
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
29
diff
changeset
|
34 |