--- a/Correctness.thy	Fri Jan 29 10:51:52 2016 +0800
+++ b/Correctness.thy	Fri Jan 29 11:01:13 2016 +0800
@@ -1,5 +1,5 @@
-theory PrioG
-imports CpsG
+theory Correctness
+imports PIPBasics
 begin
 
 text {*