diff -r aa1375b6c0eb -r 705e1e41faf7 Dynamic2static.thy
--- a/Dynamic2static.thy	Tue Aug 27 08:50:53 2013 +0800
+++ b/Dynamic2static.thy	Wed Aug 28 08:59:12 2013 +0800
@@ -1,5 +1,5 @@
 theory Dynamic2static
-imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop
+imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop
 begin
 
 context tainting_s begin