--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tainted_prop.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -0,0 +1,20 @@
+theory Tainted_prop 
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
+begin
+
+context tainting begin
+
+lemma tainted_in_current:
+  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
+apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)
+
+
+
+
+end
+
+end
+
+
+
+