# HG changeset patch
# User wenzelm
# Date 1283961606 -7200
# Node ID 39e0d3b86112ffa84ef86778e5a8b5ca0b894a31
# Parent  022f16801e4ecec37614dbd164d87a3b07d45f63
tuned proofs (based on fancy gutter icons in Isabelle/jEdit);

diff -r 022f16801e4e -r 39e0d3b86112 src/HOL/Unix/Unix.thy
--- 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 ..