| author | Christian Urban <urbanc@in.tum.de> | 
| Wed, 02 Jan 2019 21:09:05 +0000 | |
| changeset 208 | a5afc26b1d62 | 
| parent 198 | 65b178574112 | 
| permissions | -rw-r--r-- | 
| 208 | 1  | 
|
2  | 
||
3  | 
||
4  | 
Tested with Isabelle 2017  | 
|
| 146 | 5  | 
|
6  | 
||
| 
0
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
7  | 
Theories:  | 
| 
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
8  | 
=========  | 
| 
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
9  | 
|
| 195 | 10  | 
Graphs.thy A relational graph library  | 
11  | 
RTree Rooted tree graphs  | 
|
| 
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  | 
Max.thy Some generic facts about Max.  | 
| 
0
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
13  | 
Precedence_ord.thy A theory of precedences.  | 
| 
64
 
b4bcd1edbb6d
renamed files
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
52 
diff
changeset
 | 
14  | 
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
 | 
15  | 
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
 | 
16  | 
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
 | 
17  | 
Implementation.thy Properties interesting for an implementation.  | 
| 
0
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
18  | 
|
| 
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
19  | 
|
| 198 | 20  | 
The repository can be checked using Isabelle 2016-1.  | 
| 
29
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
21  | 
|
| 
45
 
fc83f79009bd
updated for Isabelle 2015
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
35 
diff
changeset
 | 
22  | 
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
 | 
23  | 
|
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
24  | 
|
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
25  | 
Othe directories are:  | 
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
26  | 
=====================  | 
| 
0
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
27  | 
|
| 
29
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
28  | 
Slides  | 
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
29  | 
Paper  | 
| 
50
 
38ad30559775
test
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
47 
diff
changeset
 | 
30  | 
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
 | 
31  | 
Literature  | 
| 47 | 32  | 
|
| 
0
 
110247f9d47e
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
33  | 
|
| 
29
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
34  | 
|
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
35  | 
|
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
36  | 
|
| 
 
408ff78ce28f
updated readme
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
0 
diff
changeset
 | 
37  | 
|
| 
30
 
7f87232d9424
test
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
29 
diff
changeset
 | 
38  | 
|
| 195 | 39  |