| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Fri, 21 Dec 2012 00:24:30 +0000 | |
| changeset 12 | 85116bc854c0 | 
| 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  |