changeset 34 | e7f850d1e08e |
parent 31 | aa1375b6c0eb |
child 43 | 137358bd4921 |
--- 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"