--- a/Correctness.thy	Tue Jan 12 08:35:36 2016 +0800
+++ b/Correctness.thy	Wed Jan 13 13:20:45 2016 +0000
@@ -2,6 +2,7 @@
 imports PIPBasics
 begin
 
+
 text {* 
   The following two auxiliary lemmas are used to reason about @{term Max}.
 *}