README
author Christian Urban <urbanc@in.tum.de>
Fri, 28 Apr 2017 15:05:36 +0100
changeset 164 613189244e72
parent 151 a79a6a286108
child 195 6b26b1fd4da5
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
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
 Precedence_ord.thy      A theory of precedences.
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
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
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
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
2e6c8d530216 Just a test change
xingyuan zhang <xingyuanzhang@126.com>
parents: 45
diff changeset
    27
  
151
Christian Urban <urbanc@in.tum.de>
parents: 150
diff changeset
    28
Test 9
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