--- a/Delete_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Delete_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -25,7 +25,7 @@
 
 lemma not_deleted_init_file:
   "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"
-apply (induct s, simp add:is_init_file_prop1)
+apply (induct s, simp add:is_file_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 apply (auto simp:is_file_simps split:option.splits)
@@ -33,7 +33,7 @@
 
 lemma not_deleted_init_dir:
   "\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f"
-apply (induct s, simp add:is_init_dir_prop1)
+apply (induct s, simp add:is_dir_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 apply (auto simp:is_dir_simps split:option.splits)
@@ -71,7 +71,7 @@
 lemma not_deleted_init_tcp_aux:
   "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
    \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
-apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1)
+apply (induct s arbitrary:p, simp add:is_tcp_sock_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 
@@ -90,7 +90,7 @@
 lemma not_deleted_init_udp_aux:
   "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
    \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
-apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1)
+apply (induct s arbitrary:p, simp add:is_udp_sock_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits