--- a/Current_files_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Current_files_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -432,6 +432,9 @@
 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
 by (clarsimp simp:current_files_def parentf_is_dir')
 
+lemma parentf_is_dir'': "\<lbrakk>f # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+by (auto intro!:parentf_is_dir)
+
 lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
 proof (induct f')
   case Nil show ?case