# HG changeset patch
# User chunhan
# Date 1378983626 -28800
# Node ID f66d61f5439db4cd8c33a3507d563371e2589ea4
# Parent  d7fab2e2a0b8807538341a40eea6931179c4d7ac
need a more general update_s2ss_sobj concept

diff -r d7fab2e2a0b8 -r f66d61f5439d S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Sep 12 18:23:38 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 12 19:00:26 2013 +0800
@@ -766,7 +766,10 @@
 apply (simp add:co2sobj_writefile_unchange alive_simps)
 done
 
-
+lemma s2ss_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
+     case (file_of_proc_fd s p fd) of
+       Some f \<Rightarrow> if ("
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
   s2ss_readfile s2ss_writefile