Tested with Isabelle 2017


Theories:
=========

 Graphs.thy              A relational graph library 
 RTree                   Rooted tree graphs 
 Max.thy                 Some generic facts about Max.
 Precedence_ord.thy      A theory of precedences.
 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 2016-1.

  isabelle build -c -v -d . PIP


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

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