
diff -r 6884b3c9284b -r e7f850d1e08e Tainted_prop.thy
--- a/Tainted_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Tainted_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -2,6 +2,8 @@
 imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop
 begin
 
+ML {*quick_and_dirty := true*}
+
 context tainting begin
 
 fun Tainted :: "t_state \<Rightarrow> t_object set"




