simple_selinux/Alive_prop.thy
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;