--- a/ROOT	Thu Oct 10 12:00:49 2013 +0800
+++ b/ROOT	Sat Oct 12 08:01:24 2013 +0800
@@ -29,4 +29,9 @@
     Sectxt_prop
     Delete_prop
     Tainted_prop
-    Co2sobj_prop
\ No newline at end of file
+    Co2sobj_prop
+
+session "s2ss" = "co2sobj" +
+  options [document = false]
+  theories
+    S2ss_prop
\ No newline at end of file

--- a/S2ss_prop.thy	Thu Oct 10 12:00:49 2013 +0800
+++ b/S2ss_prop.thy	Sat Oct 12 08:01:24 2013 +0800
@@ -677,7 +677,6 @@
 apply (rule_tac x = obj in exI, simp add:alive_simps)
 apply (drule_tac obj = obj in co2sobj_readfile, simp)
 apply (simp split:t_object.splits)
-apply (simp add:co2sobj.simps)+
 done
 
 lemma same_inode_files_prop9:
@@ -2553,25 +2552,6 @@
 apply (auto simp add:co2sobj_createshm alive_simps split:t_object.splits if_splits)
 done
 
-
-lemma s2ss_attach1:
-  "valid (Attach p h SHM_RDWR # s) \<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = "
-
-lemma s2ss_attach1:
-  "valid (Attach p h SHM_RDONLY # s) \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = "
-
-lemma s2ss_attach1:
-  "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = "
+end
 
-lemma s2ss_Detach:
-  "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = "
-
-lemma s2ss_deleteshm:
-  "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s)"
-
-
-lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
-  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
-  s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg
-  s2ss_createshm
-
+end
\ No newline at end of file