README
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 07 Jul 2016 13:32:09 +0100
changeset 133 4b717aa162fa
parent 83 61a4429e7d4d
child 146 2d66c0b0bacf
permissions -rw-r--r--
updated

Theories:
=========

 Max.thy                 Some generic facts about Max.
 Precedence_ord.thy      A theory of precedences.
 Moment.thy              The notion of moment.
 PIPDefs.thy             The formal definition of the PIP-model.
 PIPBasics.thy           Basic properties of the PIP-model.
 Correctness.thy         The correctness proof of the PIP-model.
 Implementation.thy      Properties interesting for an implementation.


The repository can be checked using Isabelle 2013-2.

  isabelle build -c -v -d . PIP


Othe directories are:
=====================

  Slides
  Paper
  Journal:     isabelle build -c -v -d . Journal
  Literature
  
Test 3