--- a/Alive_prop.thy	Wed Sep 04 09:58:30 2013 +0800
+++ b/Alive_prop.thy	Wed Sep 04 15:13:54 2013 +0800
@@ -26,14 +26,6 @@
 apply (case_tac "msgs_of_queue s q", auto)
 done
 
-lemma is_file_in_current:
-  "is_file s f \<Longrightarrow> f \<in> current_files s"
-by (auto simp:is_file_def current_files_def split:option.splits)
-
-lemma is_dir_in_current:
-  "is_dir s f \<Longrightarrow> f \<in> current_files s"
-by (auto simp:is_dir_def current_files_def split:option.splits)
-
 lemma is_tcp_in_current:
   "is_tcp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>"
 by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)