--- a/no_shm_selinux/Temp.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Temp.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -14,9 +14,12 @@
 where
   "add_ss ss so \<equiv> ss \<union> {so}"
 
+(*
 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
 where
   "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"
+*)
+
 
 (* all reachable static states(sobjects set) *)
 inductive_set static :: "t_static_state set"