--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Thu Dec 06 15:11:21 2012 +0000
@@ -0,0 +1,14 @@
+Theories:
+=========
+
+ Precedence_ord.thy      A theory of precedences.
+ Moment.thy              The notion of moment.
+ PrioGDef.thy            The formal definition of the PIP-model.
+ PrioG.thy               Basic properties of the PIP-model.
+ ExtGG.thy               The correctness proof of the PIP-model.
+ CpsG.thy                Properties interesting for an implementation.
+
+The repository can be checked using Isabelle 2011-1.
+
+  isabelle make session
+