--- a/Implementation.thy	Wed Feb 03 21:41:42 2016 +0800
+++ b/Implementation.thy	Wed Feb 03 21:51:57 2016 +0800
@@ -1,10 +1,12 @@
+(*<*)
+theory Implementation
+imports PIPBasics
+begin
+(*>*)
 section {*
   This file contains lemmas used to guide the recalculation of current precedence 
   after every system call (or system operation)
 *}
-theory Implementation
-imports PIPBasics
-begin
 
 text {* (* ddd *)
   One beauty of our modelling is that we follow the definitional extension tradition of HOL.