--- a/Implementation.thy	Wed Feb 03 22:17:29 2016 +0800
+++ b/Implementation.thy	Wed Feb 03 14:37:35 2016 +0000
@@ -1,12 +1,10 @@
-(*<*)
-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.