README
author zhangx
Wed, 27 Jan 2016 19:28:42 +0800
changeset 81 c495eb16beb6
parent 64 b4bcd1edbb6d
child 83 61a4429e7d4d
permissions -rw-r--r--
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.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