--- a/Current_files_prop.thy	Fri May 03 08:20:21 2013 +0100
+++ b/Current_files_prop.thy	Mon May 06 02:04:27 2013 +0800
@@ -539,9 +539,6 @@
 
 (******************** is_file simpset *********************)
 
-lemma is_file_nil: "is_file [] = is_init_file"
-by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)
-
 lemma is_file_open:
   "valid (Open p f flags fd opt # s) \<Longrightarrow> 
    is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))"
@@ -606,9 +603,6 @@
 
 (********* is_dir simpset **********)
 
-lemma is_dir_nil: "is_dir [] = is_init_dir"
-by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
-
 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)"
 apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext