changeset 75 | 99af1986e1e0 |
parent 74 | 271e9818b6f6 |
--- a/simple_selinux/Alive_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Alive_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -311,7 +311,6 @@ \<forall> p f. e \<noteq> UnLink p f; \<forall> p d. e \<noteq> Rmdir p d; \<forall> p d inum. e \<noteq> Mkdir p d inum; - \<forall> p f f'. e \<noteq> LinkHard p f f'; \<forall> p q. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; \<forall> p q m. e \<noteq> RecvMsg p q m;