--- a/Implementation.thy	Wed Feb 03 14:37:35 2016 +0000
+++ b/Implementation.thy	Thu Feb 04 00:43:05 2016 +0000
@@ -1,10 +1,11 @@
+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.