--- a/Co2sobj_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Co2sobj_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -2105,11 +2105,6 @@
 apply (drule cf2sfile_mkdir1, simp+)
 done
 
-lemma same_inodes_Tainted:
-  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"
-apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
-apply (auto intro:has_same_inode_Tainted)
-done
 
 lemma co2sobj_linkhard:
   "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> 
@@ -2151,9 +2146,7 @@
              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
                   same_inode_files_prop6
              dest:is_file_in_current is_dir_in_current)
-
-(* should delete has_same_inode !?!?*)
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+done
 
 lemma co2sobj_kill:
   "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"