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 \ t_object set"