# HG changeset patch
# User chunhan
# Date 1384954436 -28800
# Node ID 924ab7a4e7fa0a463cf04bc9d0a52504a4c7840f
# Parent  526ba0410662618a8fff18f94a330d61151608a2
update

diff -r 526ba0410662 -r 924ab7a4e7fa Sectxt_prop.thy
--- a/Sectxt_prop.thy	Wed Nov 20 18:51:51 2013 +0800
+++ b/Sectxt_prop.thy	Wed Nov 20 21:33:56 2013 +0800
@@ -39,6 +39,8 @@
     apply (case_tac e)
     apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
                 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+    apply (frule_tac p = nat1 in file_fds_subset_pfds)
+    apply (rule a1, auto)
     done
 qed
 
@@ -77,6 +79,8 @@
     apply (case_tac e)
     apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
                 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+    apply (frule_tac p = nat1 in file_fds_subset_pfds)
+    apply (rule a1, auto)
     done
 qed