diff -r 61a4429e7d4d -r 44df6ac30bd2 PIPDefs.thy --- a/PIPDefs.thy Wed Jan 27 13:50:02 2016 +0000 +++ b/PIPDefs.thy Thu Jan 28 13:46:45 2016 +0000 @@ -1,10 +1,11 @@ -chapter {* Definitions *} (*<*) theory PIPDefs imports Precedence_ord Moment RTree Max begin (*>*) +chapter {* Definitions *} + text {* In this section, the formal model of Priority Inheritance Protocol (PIP) is presented. The model is based on Paulson's inductive protocol verification method, where