--- a/Flask.thy	Tue May 21 10:19:51 2013 +0800
+++ b/Flask.thy	Wed May 22 15:22:50 2013 +0800
@@ -759,6 +759,14 @@
 | "deleted obj (_ # s) = deleted obj s"
 
 
+definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
+where
+  "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"
+
+
+definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
+  "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
+
 end