diff -r 8d18cfc845dd -r e832378a2ff2 no_shm_selinux/Current_prop.thy
--- a/no_shm_selinux/Current_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Current_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -94,6 +94,7 @@
 apply (simp add:file_of_pfd_is_file, simp+)
 done
 
+(*
 lemma tobj_in_init_alive:
   "tobj_in_init obj \<Longrightarrow> init_alive obj"
 by (case_tac obj, auto)
@@ -101,6 +102,7 @@
 lemma tobj_in_alive:
   "tobj_in_init obj \<Longrightarrow> alive [] obj"
 by (case_tac obj, auto simp:is_file_nil)
+*)
 
 end