--- a/PIPDefs.thy	Wed Feb 03 21:41:42 2016 +0800
+++ b/PIPDefs.thy	Wed Feb 03 21:51:57 2016 +0800
@@ -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