--- a/Flask.thy	Wed Nov 20 13:43:09 2013 +0800
+++ b/Flask.thy	Wed Nov 20 13:44:32 2013 +0800
@@ -690,7 +690,7 @@
 | "os_grant \<tau> (WriteFile p fd)                = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 
      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 
-     (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
+     (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))" 
 | "os_grant \<tau> (Execve p f fds)                = 
     (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> proc_file_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} \<and> fds \<subseteq> current_proc_fds \<tau> p *)
 (*