| 2012-04-30 | urbanc | slightly changed the definition of holdends and detached | file | diff | annotate |
| 2012-04-20 | urbanc | changes to get the files through for CU | file | diff | annotate |
| 2012-04-20 | zhang | Intuitive definition of "detached" is added to PrioG.thy. | file | diff | annotate |
| 2012-02-13 | urbanc | merged Xingyuan's changes | file | diff | annotate |
| 2012-02-12 | zhang | Correct a mistake. | file | diff | annotate |
| 2012-02-12 | zhang | runing_inversion_3 added. | file | diff | annotate |
| 2012-02-12 | urbanc | completed model section; vt has only state as argument | file | diff | annotate |
| 2012-02-10 | urbanc | more on paper | file | diff | annotate |
| 2012-01-27 | zhang | Newer version. | file | diff | annotate |
| 2012-01-24 | urbanc | initial version of the PIP formalisation | file | diff | annotate |