--- a/Implementation.thy	Thu Jan 28 13:46:45 2016 +0000
+++ b/Implementation.thy	Thu Jan 28 14:26:10 2016 +0000
@@ -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.