--- a/src/HOL/Unix/Unix.thy Wed Sep 08 16:01:06 2010 +0200
+++ b/src/HOL/Unix/Unix.thy Wed Sep 08 18:00:06 2010 +0200
@@ -945,7 +945,7 @@
from inv1 inv3 inv4 and user\<^isub>1_not_root
have not_writable: "Writable \<notin> others att"
- by (auto simp add: access_def split: option.splits if_splits)
+ by (auto simp add: access_def split: option.splits)
show ?thesis
proof cases
@@ -1044,8 +1044,7 @@
qed
finally show ?thesis .
qed
- with ys show ?thesis
- by (insert that, auto simp add: update_cons_cons_env)
+ with ys show ?thesis using that by auto
qed
also have "dir(y\<mapsto>file') \<noteq> empty" by simp
ultimately show ?thesis ..