README
author Christian Urban <urbanc@in.tum.de>
Fri, 23 Feb 2018 21:08:37 +0000
changeset 205 12a8dfcb55a7
parent 198 65b178574112
child 208 a5afc26b1d62
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
146
Christian Urban <urbanc@in.tum.de>
parents: 83
diff changeset
     1
Christian Urban <urbanc@in.tum.de>
parents: 83
diff changeset
     2
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
Theories:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
=========
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
195
6b26b1fd4da5 polished
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
     6
 Graphs.thy              A relational graph library 
6b26b1fd4da5 polished
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
     7
 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
     8
 Max.thy                 Some generic facts about Max.
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
 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
    10
 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
    11
 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
    12
 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
    13
 Implementation.thy      Properties interesting for an implementation.
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
198
65b178574112 updated
Christian Urban <urbanc@in.tum.de>
parents: 197
diff changeset
    16
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
    17
45
fc83f79009bd updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 35
diff changeset
    18
  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
    19
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    20
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    21
Othe directories are:
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    22
=====================
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
29
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    24
  Slides
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    25
  Paper
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 47
diff changeset
    26
  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
    27
  Literature
47
2e6c8d530216 Just a test change
xingyuan zhang <xingyuanzhang@126.com>
parents: 45
diff changeset
    28
  
0
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 29
diff changeset
    34
195
6b26b1fd4da5 polished
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
    35