--- a/no_shm_selinux/Flask.thy	Fri Dec 20 13:48:25 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Mon Dec 23 19:47:17 2013 +0800
@@ -542,7 +542,8 @@
 where
   "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" 
 | "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = 
-     (if (p = p' \<and> fd = fd') then Some flags else flags_of_proc_fd \<tau> p' fd')"
+     (if (p = p' \<and> fd = fd') then Some flags 
+      else flags_of_proc_fd \<tau> p' fd')"
 | "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = 
      (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"
 | "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = 
@@ -666,7 +667,7 @@
 
 
 (******* admissable check by the OS *******)
-fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+fun os_grant:: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
 where
   "os_grant \<tau> (Open p f flags fd inumopt) = (
      case inumopt of