README
author zhangx
Thu, 07 Jan 2016 22:10:06 +0800
changeset 66 2af87bb52fca
parent 64 b4bcd1edbb6d
child 83 61a4429e7d4d
permissions -rw-r--r--
Some small improvements in Correctness.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