--- a/ROOT	Thu Aug 29 10:01:24 2013 +0800
+++ b/ROOT	Thu Aug 29 13:29:32 2013 +0800
@@ -22,3 +22,11 @@
     Proc_fd_of_file_prop
     Finite_current
     New_obj_prop
+
+session "co2sobj" = "alive" + 
+  options [document = false]
+  theories
+    Sectxt_prop
+    Delete_prop
+    Tainted_prop
+    Co2sobj_prop
\ No newline at end of file