--- a/PIPBasics.thy	Fri Feb 12 17:50:24 2016 +0800
+++ b/PIPBasics.thy	Sat Feb 13 17:18:51 2016 +0800
@@ -2,6 +2,18 @@
 imports PIPDefs
 begin
 
+text {* (* ddd *)
+  Following the HOL convention of {\em definitional extension}, we have
+  given a concise and miniature model of PIP. To assure ourselves of 
+  the correctness of this model, we are going to derive a series of 
+  expected properties out of it. 
+
+  This file contains the very basic properties, useful for self-assurance, 
+  as well as for deriving more advance properties concerning 
+  the correctness and implementation of PIP.
+*}
+
+
 section {* Generic aulxiliary lemmas *}
 
 lemma rel_eqI: