README
author zhangx
Fri, 05 Feb 2016 20:11:12 +0800
changeset 109 4e59c0ce1511
parent 83 61a4429e7d4d
child 146 2d66c0b0bacf
permissions -rw-r--r--
wq_in_inv and wq_out_inv are removed, a number of loop holes need to be filled.

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