README
author zhangx
Mon, 08 Feb 2016 10:57:01 +0800
changeset 113 ce85c3c4e5bf
parent 83 61a4429e7d4d
child 146 2d66c0b0bacf
permissions -rw-r--r--
More improvements in PIPBasics.thy and Implemenation.thy.

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