--- a/no_shm_selinux/Enrich2.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -956,6 +956,17 @@
     by auto
 qed
 
+fun enrich_file_link :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_state)"
+where
+  "enrich_file_link [] tf df = []"
+
+fun enrich_file_set :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> t_state"
+where
+  "enrich_file_set [] tf df = []"
+| "enrich_file_set [] (Open p f flags fd (Some inum) # s) = 
+    
+
+
 
 
 lemma enrich_msgq_s2ss: